ULift

Statistics

Metric	Count
Definitions	0
Theorems `isAddLeftRegular_down`, `isAddLeftRegular_up`, `isAddRegular_down`, `isAddRegular_up`, `isAddRightRegular_down`, `isAddRightRegular_up`, `isLeftRegular_down`, `isLeftRegular_up`, `isRegular_down`, `isRegular_up`, `isRightRegular_down`, `isRightRegular_up`, `isSMulRegular_iff`	13
Total	13

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddLeftRegular_down` 📖	mathematical	—	`IsAddLeftRegular` `add`	—	`isAddLeftRegular_up`
`isAddLeftRegular_up` 📖	mathematical	—	`IsAddLeftRegular` `add`	—	`Equiv.comp_injective` `Equiv.injective_comp`
`isAddRegular_down` 📖	mathematical	—	`IsAddRegular` `add`	—	`isAddRegular_up`
`isAddRegular_up` 📖	mathematical	—	`IsAddRegular` `add`	—	`isAddRegular_iff` `isAddLeftRegular_up` `isAddRightRegular_up`
`isAddRightRegular_down` 📖	mathematical	—	`IsAddRightRegular` `add`	—	`isAddRightRegular_up`
`isAddRightRegular_up` 📖	mathematical	—	`IsAddRightRegular` `add`	—	`Equiv.comp_injective` `Equiv.injective_comp`
`isLeftRegular_down` 📖	mathematical	—	`IsLeftRegular` `mul`	—	`isLeftRegular_up`
`isLeftRegular_up` 📖	mathematical	—	`IsLeftRegular` `mul`	—	`Equiv.comp_injective` `Equiv.injective_comp`
`isRegular_down` 📖	mathematical	—	`IsRegular` `mul`	—	`isRegular_up`
`isRegular_up` 📖	mathematical	—	`IsRegular` `mul`	—	—
`isRightRegular_down` 📖	mathematical	—	`IsRightRegular` `mul`	—	`isRightRegular_up`
`isRightRegular_up` 📖	mathematical	—	`IsRightRegular` `mul`	—	`Equiv.comp_injective` `Equiv.injective_comp`
`isSMulRegular_iff` 📖	mathematical	—	`IsSMulRegular` `smul`	—	`Equiv.comp_injective` `Equiv.injective_comp`

---