Basic
📁 Source: Mathlib/Algebra/AffineMonoid/Basic.lean
Statistics
| Metric | Count |
|---|---|
| 2 | |
| 6 | |
| Total | 8 |
IsAffineAddMonoid
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
toFG 📖 | mathematical | — | AddMonoid.FGAddCommMonoid.toAddMonoid | — | — |
toIsAddTorsionFree 📖 | mathematical | — | IsAddTorsionFreeAddCommMonoid.toAddMonoid | — | — |
toIsCancelAdd 📖 | mathematical | — | IsCancelAddAddCommMagma.toAddAddCommSemigroup.toAddCommMagmaAddCommMonoid.toAddCommSemigroup | — | — |
IsAffineMonoid
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
toFG 📖 | mathematical | — | Monoid.FGCommMonoid.toMonoid | — | — |
toIsCancelMul 📖 | mathematical | — | IsCancelMulMulOne.toMulMulOneClass.toMulOneMonoid.toMulOneClassCommMonoid.toMonoid | — | — |
toIsMulTorsionFree 📖 | mathematical | — | IsMulTorsionFreeCommMonoid.toMonoid | — | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
IsAffineAddMonoid 📖 | CompData | — |
IsAffineMonoid 📖 | CompData | — |
---