Theorems · Definition · order theory
AddSubgroup.toIntSubmodule
{M : Type u_3} → [inst : AddCommGroup M] → AddSubgroup M ≃o Submodule ℤ MAn additive subgroup is equivalent to a ℤ-submodule.
- Defined in
- Mathlib.Algebra.Module.Submodule.Lattice
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 42 from the axioms · uses propext, Quot.sound
- Assumes
- AddCommGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- Submodulestatement · cited by 7,192
- AddSubgroupstatement and proof · cited by 3,232
- OrderIsostatement · cited by 874
- Submodule.toAddSubgroupproof · cited by 106
- AddSubgroup.toAddSubmonoidproof · cited by 91
Cited by26
Results whose statement or proof uses this declaration.
- NumberField.absNorm_differentIdealproof · cited by 4
- Module.Basis.addSubgroupOfClosurestatement and proof · cited by 4
- PeriodPair.weierstrassP_add_coeproof · cited by 3
- iSupIndep_of_dfinsuppSumAddHom_injective'proof · cited by 2
- Module.Basis.addSubgroupOfClosure_applystatement · cited by 2
- AddSubgroup.relIndex_eq_natAbs_detstatement and proof · cited by 2
- AddSubgroup.toIntSubmodule_toAddSubgroupstatement and proof · cited by 2
- Submodule.toIntSubmodule_toAddSubgroupstatement · cited by 1
- Module.Basis.addSubgroupOfClosure_repr_applystatement and proof · cited by 1
- finrank_quotient_torsion_eqstatement and proof · cited by 1
- AddSubgroup.index_eq_natAbs_detproof · cited by 1
- Submodule.fg_toAddSubgroupproof · cited by 1