Commit 2025-02-10 17:54 5b5cbabe

View on Github →

chore(Algebra/Module): process porting notes (#21634)

Estimated changes

Modified Mathlib/Algebra/Module/Defs.lean

Modified Mathlib/Algebra/Module/End.lean

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

modified theorem LinearEquiv.toFun_eq_coe

Modified Mathlib/Algebra/Module/Equiv/Opposite.lean

Modified Mathlib/Algebra/Module/GradedModule.lean

Modified Mathlib/Algebra/Module/Injective.lean

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

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

Modified Mathlib/Algebra/Module/PID.lean

Modified Mathlib/Algebra/Module/Pi.lean

Modified Mathlib/Algebra/Module/PointwisePi.lean

Modified Mathlib/Algebra/Module/RingHom.lean

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

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

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

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

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

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

Modified Mathlib/Algebra/Module/Torsion.lean

deleted def Submodule.torsion'AddSubMonoid

Modified Mathlib/Algebra/Module/ULift.lean