Commit 2022-06-09 13:27 c2bb59e5

View on Github →

feat(algebra/module/torsion.lean): various lemmas about torsion modules (#14573) An intermediate PR for various lemmas about torsion modules needed at #13524

Estimated changes

Modified src/algebra/module/torsion.lean

added theorem ideal.mem_torsion_of_iff

added theorem ideal.quot_torsion_of_equiv_span_singleton_apply_mk

added theorem ideal.sup_eq_top_iff_is_coprime

added def ideal.torsion_of

deleted theorem mem_torsion_of_iff

added theorem module.is_torsion_by_iff_torsion_by_eq_top

added theorem module.is_torsion_by_set_iff_is_torsion_by_span

added theorem module.is_torsion_by_set_iff_torsion_by_set_eq_top

added theorem module.is_torsion_by_singleton_iff

added theorem module.is_torsion_by_span_singleton_iff

deleted theorem quot_torsion_of_equiv_span_singleton_apply_mk

added theorem submodule.exists_is_torsion_by

added theorem submodule.is_torsion_by_ideal_of_finite_of_is_torsion

deleted theorem submodule.is_torsion_by_iff_torsion_by_eq_top

deleted theorem submodule.is_torsion_by_set_iff_is_torsion_by_span

deleted theorem submodule.is_torsion_by_set_iff_torsion_by_set_eq_top

deleted theorem submodule.is_torsion_by_singleton_iff

deleted theorem submodule.is_torsion_by_span_singleton_iff

added def submodule.p_order

added theorem submodule.pow_p_order_smul

added theorem submodule.sup_indep_torsion_by

added theorem submodule.sup_indep_torsion_by_ideal

added theorem submodule.supr_torsion_by_ideal_eq_torsion_by_infi

deleted theorem submodule.torsion_by_independent

added theorem submodule.torsion_by_is_internal

added theorem submodule.torsion_by_set_is_internal

added theorem submodule.torsion_gc

deleted theorem submodule.torsion_is_internal

deleted def torsion_of

Modified src/ring_theory/ideal/operations.lean

added theorem ideal.prod_mem_prod