Commit 2023-05-26 05:11 78320330

View on Github →

feat: port Algebra.Module.Torsion (#4365)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/Torsion.lean

added theorem AddMonoid.isTorsion_iff_isTorsion_int

added theorem AddMonoid.isTorsion_iff_isTorsion_nat

added theorem Ideal.CompleteLattice.Independent.linear_independent'

added theorem Ideal.Quotient.torsionBy_eq_span_singleton

added theorem Ideal.mem_torsionOf_iff

added theorem Ideal.quotTorsionOfEquivSpanSingleton_apply_mk

added def Ideal.torsionOf

added theorem Ideal.torsionOf_eq_bot_iff_of_noZeroSMulDivisors

added theorem Ideal.torsionOf_eq_top_iff

added theorem Ideal.torsionOf_zero

added def Module.IsTorsion'

added def Module.IsTorsion

added def Module.IsTorsionBy

added def Module.IsTorsionBySet.hasSMul

added theorem Module.IsTorsionBySet.mk_smul

added def Module.IsTorsionBySet.module

added def Module.IsTorsionBySet

added theorem Module.isTorsionBySet_annihilator_top

added theorem Module.isTorsionBySet_iff_is_torsion_by_span

added theorem Module.isTorsionBySet_iff_torsionBySet_eq_top

added theorem Module.isTorsionBySet_singleton_iff

added theorem Module.isTorsionBySet_span_singleton_iff

added theorem Module.isTorsionBy_iff_torsionBy_eq_top

added theorem Submodule.QuotientTorsion.torsion_eq_bot

added theorem Submodule.annihilator_top_inter_nonZeroDivisors

added theorem Submodule.coe_torsion_eq_annihilator_ne_bot

added theorem Submodule.exists_isTorsionBy

added theorem Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf

added theorem Submodule.iSup_torsionBy_eq_torsionBy_prod

added theorem Submodule.isTorsion'_iff_torsion'_eq_top

added theorem Submodule.isTorsion'_powers_iff

added theorem Submodule.mem_torsion'_iff

added theorem Submodule.mem_torsionBySet_iff

added theorem Submodule.mem_torsionBy_iff

added theorem Submodule.mem_torsion_iff

added theorem Submodule.noZeroSMulDivisors_iff_torsion_eq_bot

added def Submodule.pOrder

added theorem Submodule.pow_pOrder_smul

added theorem Submodule.smul_coe_torsionBy

added theorem Submodule.smul_torsionBy

added theorem Submodule.supIndep_torsionBy

added theorem Submodule.supIndep_torsionBySet_ideal

added def Submodule.torsion'

added def Submodule.torsion'AddSubMonoid

added theorem Submodule.torsion'_isTorsion'

added theorem Submodule.torsion'_torsion'_eq_top

added def Submodule.torsion

added theorem Submodule.torsionBy.mk_ideal_smul

added theorem Submodule.torsionBy.mk_smul

added def Submodule.torsionBy

added theorem Submodule.torsionBySet.mk_smul

added def Submodule.torsionBySet

added theorem Submodule.torsionBySet_eq_torsionBySet_span

added theorem Submodule.torsionBySet_isInternal

added theorem Submodule.torsionBySet_isTorsionBySet

added theorem Submodule.torsionBySet_le_torsionBySet_of_subset

added theorem Submodule.torsionBySet_singleton_eq

added theorem Submodule.torsionBySet_span_singleton_eq

added theorem Submodule.torsionBySet_torsionBySet_eq_top

added theorem Submodule.torsionBySet_univ

added theorem Submodule.torsionBy_isInternal

added theorem Submodule.torsionBy_isTorsionBy

added theorem Submodule.torsionBy_le_torsionBy_of_dvd

added theorem Submodule.torsionBy_one

added theorem Submodule.torsionBy_torsionBy_eq_top

added theorem Submodule.torsion_gc

added theorem Submodule.torsion_isTorsion

added theorem Submodule.torsion_torsion_eq_top