InjSurj

Statistics

Metric	Count
Definitions `addCancelCommMonoid`, `addCancelMonoid`, `addCommGroup`, `addCommMagma`, `addCommMonoid`, `addCommSemigroup`, `addGroup`, `addLeftCancelMonoid`, `addLeftCancelSemigroup`, `addMonoid`, `addRightCancelMonoid`, `addRightCancelSemigroup`, `addSemigroup`, `addZeroClass`, `cancelCommMonoid`, `cancelMonoid`, `commGroup`, `commMagma`, `commMonoid`, `commSemigroup`, `divInvMonoid`, `divInvOneMonoid`, `divisionCommMonoid`, `divisionMonoid`, `group`, `invOneClass`, `involutiveInv`, `involutiveNeg`, `leftCancelMonoid`, `leftCancelSemigroup`, `monoid`, `mulOneClass`, `negZeroClass`, `rightCancelMonoid`, `rightCancelSemigroup`, `semigroup`, `subNegMonoid`, `subNegZeroMonoid`, `subtractionCommMonoid`, `subtractionMonoid`, `addCommGroup`, `addCommMagma`, `addCommMonoid`, `addCommSemigroup`, `addGroup`, `addMonoid`, `addSemigroup`, `addZeroClass`, `commGroup`, `commMagma`, `commMonoid`, `commSemigroup`, `divInvMonoid`, `group`, `involutiveInv`, `involutiveNeg`, `monoid`, `mulOneClass`, `semigroup`, `subNegMonoid`	60
Theorems `isCancelAdd`, `isCancelMul`, `isLeftCancelAdd`, `isLeftCancelMul`, `isRightCancelAdd`, `isRightCancelMul`	6
Total	66

Name	Kind	Assumes	Proves	Validates	Depends On
`isCancelAdd` 📖	mathematical	—	`IsCancelAdd`	—	`isLeftCancelAdd` `IsCancelAdd.toIsLeftCancelAdd` `isRightCancelAdd` `IsCancelAdd.toIsRightCancelAdd`
`isCancelMul` 📖	mathematical	—	`IsCancelMul`	—	`isLeftCancelMul` `IsCancelMul.toIsLeftCancelMul` `isRightCancelMul` `IsCancelMul.toIsRightCancelMul`
`isLeftCancelAdd` 📖	mathematical	—	`IsLeftCancelAdd`	—	`add_left_cancel`
`isLeftCancelMul` 📖	mathematical	—	`IsLeftCancelMul`	—	`mul_left_cancel`
`isRightCancelAdd` 📖	mathematical	—	`IsRightCancelAdd`	—	`add_right_cancel`
`isRightCancelMul` 📖	mathematical	—	`IsRightCancelMul`	—	`mul_right_cancel`

---