Revision #979 → #2509 · back to history
modifiedUnits form abelian multiplicative groupd38757e30e31
| Field | From #979 | To #2509 |
|---|
| mathlib.decl | instCommGroupUnits | Units.instCommGroupUnits |
| provenance | ai | ai-moderated |
modifiedAbelian groups equal Z-modulesc36b3e993ef2
| Field | From #979 | To #2509 |
|---|
| mathlib.decl | forget₂AddCommGroupIsEquivalence | ModuleCat.forget₂AddCommGroupIsEquivalence |
| provenance | ai | ai-moderated |
modifiedRank zero iff torsion668f2fdeb05a
| Field | From #979 | To #2509 |
|---|
| mathlib.decl | Module.rank_eq_zero_iff_isTorsion | rank_eq_zero_iff_isTorsion |
| provenance | ai | ai-moderated |
modifiedInfinite cyclic group24086b40a168
| Field | From #979 | To #2509 |
|---|
| mathlib.decl | Int.instIsAddCyclic | instIsAddCyclicInt |
| provenance | ai | ai-moderated |
modifiedTorsion-free abelian group9634b5f0a417
| Field | From #979 | To #2509 |
|---|
| mathlib.decl | Monoid.IsTorsionFree | IsMulTorsionFree |
| provenance | ai | ai-moderated |
modifiedRank 0 groups are periodic0922184fdff9
| Field | From #979 | To #2509 |
|---|
| mathlib.decl | Module.rank_eq_zero_iff_isTorsion | rank_eq_zero_iff_isTorsion |
| provenance | ai | ai-moderated |