Commit 2026-01-12 13:34 f56df434

View on Github →

feat(Algebra): more Module.IsTorsionFree API (#33871) This will be used in #30563.

Estimated changes

Modified Counterexamples/DimensionPolynomial.lean

Modified Mathlib/Algebra/Algebra/Basic.lean

added theorem Module.IsTorsionFree.of_faithfulSMul

added theorem Module.IsTorsionFree.trans_faithfulSMul

added theorem Module.isTorsionFree_iff_algebraMap_injective

added theorem Module.isTorsionFree_iff_faithfulSMul

added theorem isSMulRegular_algebraMap_iff

Modified Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

Modified Mathlib/Algebra/Module/Torsion/Basic.lean

added theorem Submodule.isTorsionFree_iff_torsion_eq_bot

Modified Mathlib/Algebra/Module/Torsion/Free.lean

added theorem Module.IsTorsionFree.comap

added theorem Module.IsTorsionFree.of_smul_eq_zero

added theorem Module.isTorsionFree_iff_smul_eq_zero

Modified Mathlib/Algebra/Module/TransferInstance.lean

Modified Mathlib/Algebra/MonoidAlgebra/Module.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean

Modified Mathlib/Algebra/QuadraticAlgebra/Defs.lean

Modified Mathlib/Algebra/Regular/SMul.lean

added theorem isSMulRegular_map

Modified Mathlib/Algebra/Ring/Subring/Defs.lean

added theorem Subring.mk_eq_zero

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/Data/Finsupp/SMul.lean

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

added theorem IsIntegralClosure.isTorsionFree

Modified Mathlib/RingTheory/LocalRing/LocalSubring.lean

Modified Mathlib/RingTheory/Regular/IsSMulRegular.lean

deleted theorem isSMulRegular_algebraMap_iff

Modified Mathlib/RingTheory/Valuation/Extension.lean

added theorem Valuation.HasExtension.mk_smul_mk