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, finiteIndex_range_nsmulAddMonoidHom_of_fg, isFiniteRelIndex_map_nsmulAddMonoidHom_of_fg, equiv_free_prod_prod_multiplicative_zmod, equiv_prod_multiplicative_zmod_of_finite, finite_of_fg_torsion, finite_of_fg_torsion, finiteIndex_range_powMonoidHom_of_fg, isFiniteRelIndex_map_powMonoidHom_of_fg, fg_toAddSubgroup, isFiniteRelIndex_of_map_linearMapMulLeft_le	14
Total	14

AddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_directSum_zmod_of_finite 📖	mathematical	—	Fintype AddEquiv DirectSum ZMod Monoid.toPow 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 Finsupp.instSubsingleton Fin.isEmpty' Fintype.false Int.infinite Finsupp.single_eq_same
equiv_directSum_zmod_of_finite' 📖	mathematical	—	Fintype 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	—	Fintype AddEquiv Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing DirectSum ZMod Monoid.toPow 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

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteIndex_range_nsmulAddMonoidHom_of_fg 📖	mathematical	—	FiniteIndex AddCommGroup.toAddGroup AddMonoidHom.range nsmulAddMonoidHom AddCommGroup.toAddCommMonoid	—	finiteIndex_iff_finite_quotient AddCommGroup.finite_of_fg_torsion QuotientAddGroup.fg normal_of_comm AddCommGroup.isTorsion_quotient_range_nsmulAddMonoidHom
isFiniteRelIndex_map_nsmulAddMonoidHom_of_fg 📖	mathematical	FG AddCommGroup.toAddGroup	IsFiniteRelIndex AddCommGroup.toAddGroup map nsmulAddMonoidHom AddCommGroup.toAddCommMonoid	—	isFiniteRelIndex_iff_finiteIndex ext mem_addSubgroupOf mem_map AddMonoidHom.mem_range AddGroup.fg_iff_addSubgroup_fg finiteIndex_range_nsmulAddMonoidHom_of_fg

CommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_free_prod_prod_multiplicative_zmod 📖	mathematical	—	Fintype MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid toGroup Prod.instMul Pi.instMul Multiplicative Multiplicative.mul ZMod Monoid.toPow 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	—	Fintype 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

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteIndex_range_powMonoidHom_of_fg 📖	mathematical	—	FiniteIndex CommGroup.toGroup MonoidHom.range powMonoidHom CommGroup.toCommMonoid	—	finiteIndex_iff_finite_quotient CommGroup.finite_of_fg_torsion QuotientGroup.fg normal_of_comm CommGroup.isTorsion_quotient_range_powMonoidHom
isFiniteRelIndex_map_powMonoidHom_of_fg 📖	mathematical	FG CommGroup.toGroup	IsFiniteRelIndex CommGroup.toGroup map powMonoidHom CommGroup.toCommMonoid	—	isFiniteRelIndex_iff_finiteIndex ext Group.fg_iff_subgroup_fg finiteIndex_range_powMonoidHom_of_fg

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_toAddSubgroup 📖	mathematical	FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	AddSubgroup.FG AddCommGroup.toAddGroup toAddSubgroup CommRing.toRing	—	AddSubgroup.toIntSubmodule_toAddSubgroup fg_iff_addSubgroup_fg FG.restrictScalars AddCommGroup.intIsScalarTower
isFiniteRelIndex_of_map_linearMapMulLeft_le 📖	mathematical	FG CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.mulLeft Algebra.to_smulCommClass AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	AddSubgroup.IsFiniteRelIndex AddCommGroup.toAddGroup Ring.toAddCommGroup CommRing.toRing toAddSubgroup Algebra.toModule CommRing.toCommSemiring CommSemiring.toSemiring	—	RingHomSurjective.ids Algebra.to_smulCommClass fg_toAddSubgroup AddSubgroup.isFiniteRelIndex_map_nsmulAddMonoidHom_of_fg AddSubgroup.isFiniteRelIndex_of_le SetLike.le_def instIsConcreteLE neg_mem nsmul_eq_mul

---

← Back to Index