Commit 2024-05-24 03:14 124ce2b4

View on Github →

Feat(Algebra/Module/Torsion): Fill out isTorsionBy API. (#13130) This PR connects regularity to torsionBy and fills out some missing parallels between IsTorsionBySet and IsTorsionBy.

Estimated changes

Modified Mathlib/Algebra/Module/Torsion.lean

added theorem Module.IsTorsionBy.mk_smul

added theorem Module.IsTorsionBy.quotient

modified def Module.IsTorsionBySet.hasSMul

modified theorem Module.IsTorsionBySet.mk_smul

modified def Module.IsTorsionBySet.module

added theorem Module.IsTorsionBySet.quotient

added theorem Module.isTorsionBySet_iff_subseteq_ker_lsmul

added theorem Module.isTorsionBySet_quotient_ideal_smul

added theorem Module.isTorsionBySet_quotient_iff

added theorem Module.isTorsionBySet_quotient_set_smul

added theorem Module.isTorsionBy_iff_mem_ker_lsmul

added theorem Module.isTorsionBy_quotient_element_smul

added theorem Module.isTorsionBy_quotient_iff

modified theorem Submodule.torsionBySet_isTorsionBySet

modified theorem Submodule.torsionBy_isTorsionBy

added theorem isSMulRegular_iff_torsionBy_top_eq_bot