InjSurj
📁 Source: Mathlib/Algebra/GroupWithZero/InjSurj.lean
Statistics
| Metric | Count |
|---|---|
| 14 | |
| 4 | |
| Total | 18 |
Function.Injective
Definitions
| Name | Category | Theorems |
|---|---|---|
commGroupWithZero 📖 | CompOp | — |
commMonoidWithZero 📖 | CompOp | — |
groupWithZero 📖 | CompOp | — |
monoidWithZero 📖 | CompOp | — |
mulZeroClass 📖 | CompOp | — |
mulZeroOneClass 📖 | CompOp | — |
semigroupWithZero 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
isCancelMulZero 📖 | mathematical | — | IsCancelMulZero | — | isLeftCancelMulZeroIsCancelMulZero.toIsLeftCancelMulZeroisRightCancelMulZeroIsCancelMulZero.toIsRightCancelMulZero |
isLeftCancelMulZero 📖 | mathematical | — | IsLeftCancelMulZero | — | mul_left_cancel₀ |
isRightCancelMulZero 📖 | mathematical | — | IsRightCancelMulZero | — | mul_right_cancel₀ |
noZeroDivisors 📖 | mathematical | — | NoZeroDivisors | — | NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero |
Function.Surjective
Definitions
| Name | Category | Theorems |
|---|---|---|
commGroupWithZero 📖 | CompOp | — |
commMonoidWithZero 📖 | CompOp | — |
groupWithZero 📖 | CompOp | — |
monoidWithZero 📖 | CompOp | — |
mulZeroClass 📖 | CompOp | — |
mulZeroOneClass 📖 | CompOp | — |
semigroupWithZero 📖 | CompOp | — |
---