Synonym
📁 Source: Mathlib/Algebra/Order/GroupWithZero/Synonym.lean
Statistics
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
instCommGroupWithZeroLex 📖 | CompOp | — |
instCommGroupWithZeroOrderDual 📖 | CompOp | — |
instCommMonoidWithZeroLex 📖 | CompOp | — |
instCommMonoidWithZeroOrderDual 📖 | CompOp | — |
instGroupWithZeroLex 📖 | CompOp | — |
instGroupWithZeroOrderDual 📖 | CompOp | — |
instMonoidWithZeroLex 📖 | CompOp | — |
instMonoidWithZeroOrderDual 📖 | CompOp | — |
instMulZeroClassLex 📖 | CompOp | — |
instMulZeroClassOrderDual 📖 | CompOp | — |
instMulZeroOneClassLex 📖 | CompOp | — |
instMulZeroOneClassOrderDual 📖 | CompOp | — |
instSemigroupWithZeroLex 📖 | CompOp | — |
instSemigroupWithZeroOrderDual 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
instIsCancelMulZeroLex 📖 | mathematical | — | IsCancelMulZeroLexinstMulLexinstZeroLex | — | — |
instIsCancelMulZeroOrderDual 📖 | mathematical | — | IsCancelMulZeroOrderDualinstMulOrderDualinstZeroOrderDual | — | — |
instIsLeftCancelMulZeroLex 📖 | mathematical | — | IsLeftCancelMulZeroLexinstMulLexinstZeroLex | — | — |
instIsLeftCancelMulZeroOrderDual 📖 | mathematical | — | IsLeftCancelMulZeroOrderDualinstMulOrderDualinstZeroOrderDual | — | — |
instIsRightCancelMulZeroLex 📖 | mathematical | — | IsRightCancelMulZeroLexinstMulLexinstZeroLex | — | — |
instIsRightCancelMulZeroOrderDual 📖 | mathematical | — | IsRightCancelMulZeroOrderDualinstMulOrderDualinstZeroOrderDual | — | — |
instNoZeroDivisorsLex 📖 | mathematical | — | NoZeroDivisorsLexinstMulLexinstZeroLex | — | — |
instNoZeroDivisorsOrderDual 📖 | mathematical | — | NoZeroDivisorsOrderDualinstMulOrderDualinstZeroOrderDual | — | — |
---