Documentation Verification Report

Synonym

📁 Source: Mathlib/Algebra/Order/GroupWithZero/Synonym.lean

Statistics

Metric	Count
Definitions `instCommGroupWithZero`, `instCommMonoidWithZero`, `instGroupWithZero`, `instMonoidWithZero`, `instMulZeroClass`, `instMulZeroOneClass`, `instSemigroupWithZero`, `instCommGroupWithZeroLex`, `instCommMonoidWithZeroLex`, `instGroupWithZeroLex`, `instMonoidWithZeroLex`, `instMulZeroClassLex`, `instMulZeroOneClassLex`, `instSemigroupWithZeroLex`	14
Theorems `instIsCancelMulZero`, `instIsLeftCancelMulZero`, `instIsRightCancelMulZero`, `instNoZeroDivisors`, `instIsCancelMulZeroLex`, `instIsLeftCancelMulZeroLex`, `instIsRightCancelMulZeroLex`, `instNoZeroDivisorsLex`	8
Total	22

OrderDual

Definitions

Name	Category	Theorems
`instCommGroupWithZero` 📖	CompOp	—
`instCommMonoidWithZero` 📖	CompOp	—
`instGroupWithZero` 📖	CompOp	—
`instMonoidWithZero` 📖	CompOp	—
`instMulZeroClass` 📖	CompOp	—
`instMulZeroOneClass` 📖	CompOp	—
`instSemigroupWithZero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCancelMulZero` 📖	mathematical	—	`IsCancelMulZero` `OrderDual` `instMul` `instZero`	—	`instIsLeftCancelMulZero` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsRightCancelMulZero` `IsCancelMulZero.toIsRightCancelMulZero`
`instIsLeftCancelMulZero` 📖	mathematical	—	`IsLeftCancelMulZero` `OrderDual` `instMul` `instZero`	—	`IsLeftCancelMulZero.mul_left_cancel_of_ne_zero`
`instIsRightCancelMulZero` 📖	mathematical	—	`IsRightCancelMulZero` `OrderDual` `instMul` `instZero`	—	`IsRightCancelMulZero.mul_right_cancel_of_ne_zero`
`instNoZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `OrderDual` `instMul` `instZero`	—	`NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero`

(root)

Definitions

Name	Category	Theorems
`instCommGroupWithZeroLex` 📖	CompOp	—
`instCommMonoidWithZeroLex` 📖	CompOp	—
`instGroupWithZeroLex` 📖	CompOp	—
`instMonoidWithZeroLex` 📖	CompOp	—
`instMulZeroClassLex` 📖	CompOp	—
`instMulZeroOneClassLex` 📖	CompOp	—
`instSemigroupWithZeroLex` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCancelMulZeroLex` 📖	mathematical	—	`IsCancelMulZero` `Lex` `instMulLex` `instZeroLex`	—	—
`instIsLeftCancelMulZeroLex` 📖	mathematical	—	`IsLeftCancelMulZero` `Lex` `instMulLex` `instZeroLex`	—	—
`instIsRightCancelMulZeroLex` 📖	mathematical	—	`IsRightCancelMulZero` `Lex` `instMulLex` `instZeroLex`	—	—
`instNoZeroDivisorsLex` 📖	mathematical	—	`NoZeroDivisors` `Lex` `instMulLex` `instZeroLex`	—	—

---

← Back to Index