Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 14:49 7302e116

View on Github →

feat(algebra/module/torsion): define torsion submodules (#12027) This file defines the a-torsion and torsion submodules for a R-module M and gives some basic properties. (The ultimate goal I'm working on is to classify the finitely-generated modules over a PID).

Estimated changes

Modified src/algebra/group/basic.lean

added theorem exists_npow_eq_one_of_zpow_eq_one

Created src/algebra/module/torsion.lean

added theorem add_monoid.is_torsion_iff_is_torsion_int

added theorem add_monoid.is_torsion_iff_is_torsion_nat

added def module.is_torsion'

added def module.is_torsion

added def module.is_torsion_by

added theorem submodule.coe_torsion_eq_annihilator_ne_bot

added theorem submodule.is_torsion'_iff_torsion'_eq_top

added theorem submodule.is_torsion_by_iff_torsion_by_eq_top

added theorem submodule.mem_torsion'_iff

added theorem submodule.mem_torsion_by_iff

added theorem submodule.mem_torsion_iff

added theorem submodule.no_zero_smul_divisors_iff_torsion_eq_bot

added theorem submodule.quotient_torsion.torsion_eq_bot

added theorem submodule.smul_coe_torsion_by

added theorem submodule.smul_torsion_by

added def submodule.torsion'

added theorem submodule.torsion'_is_torsion'

added theorem submodule.torsion'_torsion'_eq_top

added def submodule.torsion

added theorem submodule.torsion_by.mk_smul

added def submodule.torsion_by

added theorem submodule.torsion_by_is_torsion_by

added theorem submodule.torsion_by_torsion_by_eq_top

added theorem submodule.torsion_is_torsion

added theorem submodule.torsion_torsion_eq_top