Commit 2022-05-04 11:10 6c7b880e

View on Github →

feat(algebra/module/torsion): torsion ideal, decomposition lemma (#13414) Defines the torsion ideal of an element in a module, and also shows a decomposition lemma for torsion modules.

Estimated changes

Modified src/algebra/module/torsion.lean

added theorem ideal.quotient.torsion_by_eq_span_singleton

added theorem mem_torsion_of_iff

added def module.is_torsion_by_set.has_scalar

added theorem module.is_torsion_by_set.mk_smul

added def module.is_torsion_by_set.module

added def module.is_torsion_by_set

added theorem quot_torsion_of_equiv_span_singleton_apply_mk

added theorem submodule.is_torsion'_powers_iff

added theorem submodule.is_torsion_by_set_iff_is_torsion_by_span

added theorem submodule.is_torsion_by_set_iff_torsion_by_set_eq_top

added theorem submodule.is_torsion_by_singleton_iff

added theorem submodule.is_torsion_by_span_singleton_iff

added theorem submodule.mem_torsion_by_set_iff

added theorem submodule.supr_torsion_by_eq_torsion_by_prod

modified theorem submodule.torsion_by.mk_smul

added theorem submodule.torsion_by_independent

added theorem submodule.torsion_by_le_torsion_by_of_dvd

added theorem submodule.torsion_by_one

added theorem submodule.torsion_by_set.mk_smul

added def submodule.torsion_by_set

added theorem submodule.torsion_by_set_eq_torsion_by_span

added theorem submodule.torsion_by_set_is_torsion_by_set

added theorem submodule.torsion_by_set_le_torsion_by_set_of_subset

added theorem submodule.torsion_by_set_torsion_by_set_eq_top

added theorem submodule.torsion_by_singleton_eq

added theorem submodule.torsion_by_span_singleton_eq

added theorem submodule.torsion_by_univ

added theorem submodule.torsion_is_internal

added def torsion_of

Modified src/ring_theory/coprime/lemmas.lean

modified theorem exists_sum_eq_one_iff_pairwise_coprime'

modified theorem exists_sum_eq_one_iff_pairwise_coprime

modified theorem pairwise_coprime_iff_coprime_prod