Theorems · Theorem · group theory
AddSubgroup.finiteIndex_range_nsmulAddMonoidHom_of_fg
∀ (A : Type u_1) [inst : AddCommGroup A] [AddGroup.FG A] {n : ℕ}, n ≠ 0 → (nsmulAddMonoidHom n).range.FiniteIndex- Defined in
- Mathlib.GroupTheory.FiniteAbelian.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommGroupAddGroup.FG
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- HasQuotient.Quotientproof · cited by 2,301
- AddMonoidHom.rangestatement and proof · cited by 142
- AddSubgroup.FiniteIndexstatement · cited by 66
- AddGroup.FGstatement and proof · cited by 37
- nsmulAddMonoidHomstatement and proof · cited by 24
- AddCommGroup.finite_of_fg_isAddTorsionproof · cited by 2
- AddCommGroup.isAddTorsion_quotient_range_nsmulAddMonoidHomproof · cited by 2
- AddSubgroup.finiteIndex_iff_finite_quotientproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- AddSubgroup.isFiniteRelIndex_map_nsmulAddMonoidHom_of_fgproof · cited by 1