Documentation Verification Report

Basic

📁 Source: Mathlib/GroupTheory/FiniteAbelian/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `equiv_directSum_zmod_of_finite`, `equiv_directSum_zmod_of_finite'`, `equiv_free_prod_directSum_zmod`, `finite_of_fg_torsion`, `equiv_free_prod_prod_multiplicative_zmod`, `equiv_prod_multiplicative_zmod_of_finite`, `finite_of_fg_torsion`, `finite_of_fg_torsion`	8
Total	8

AddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv_directSum_zmod_of_finite` 📖	mathematical	—	`AddEquiv` `DirectSum` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `instAddCommMonoidDirectSum`	—	`nonempty_fintype` `equiv_free_prod_directSum_zmod` `AddGroup.fg_of_finite` `Unique.instSubsingleton` `Fin.isEmpty'` `Fintype.false` `Int.infinite` `Finsupp.single_eq_same`
`equiv_directSum_zmod_of_finite'` 📖	mathematical	—	`AddEquiv` `DirectSum` `ZMod` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `instAddCommMonoidDirectSum`	—	`equiv_directSum_zmod_of_finite` `one_lt_pow₀` `Nat.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.Prime.one_lt`
`equiv_free_prod_directSum_zmod` 📖	mathematical	—	`AddEquiv` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `DirectSum` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `ZMod.commRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `toAddCommMonoid` `Prod.instAdd` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `instAddCommMonoidDirectSum`	—	`RingHomInvPair.ids` `Module.equiv_free_prod_directSum` `EuclideanDomain.to_principal_ideal_domain` `Int.instIsDomain` `Module.Finite.iff_addGroup_fg` `Int.prime_iff_natAbs_prime` `irreducible_iff_prime` `Int.instIsCancelMulZero` `UniqueFactorizationMonoid.instDecompositionMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid`
`finite_of_fg_torsion` 📖	mathematical	`AddMonoid.IsTorsion` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddGroup`	`Finite`	—	`Module.finite_of_fg_torsion` `Module.Finite.iff_addGroup_fg` `AddMonoid.isTorsion_iff_isTorsion_int`

CommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv_free_prod_prod_multiplicative_zmod` 📖	mathematical	—	`MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `Prod.instMul` `Pi.instMul` `Multiplicative` `Multiplicative.mul` `ZMod` `Monoid.toNatPow` `Nat.instMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	`AddCommGroup.equiv_free_prod_directSum_zmod` `AddGroup.fg_of_group_fg` `Finite.of_fintype`
`equiv_prod_multiplicative_zmod_of_finite` 📖	mathematical	—	`MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup` `Pi.instMul` `Multiplicative` `ZMod` `Multiplicative.mul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing`	—	`AddCommGroup.equiv_directSum_zmod_of_finite'` `instFiniteAdditive`
`finite_of_fg_torsion` 📖	mathematical	`Monoid.IsTorsion` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toGroup`	`Finite`	—	`Finite.of_equiv` `AddCommGroup.finite_of_fg_torsion` `AddGroup.fg_of_group_fg`

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_of_fg_torsion` 📖	mathematical	`IsTorsion` `Int.instSemiring` `AddCommGroup.toAddCommMonoid`	`Finite`	—	`RingHomInvPair.ids` `equiv_directSum_of_isTorsion` `EuclideanDomain.to_principal_ideal_domain` `Int.instIsDomain` `Finite.of_equiv` `Pi.finite` `Finite.of_fintype` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Int.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Irreducible.ne_zero`

---

← Back to Index