Commit 2026-01-06 19:16 b0546921

View on Github →

chore(Algebra): some cleanup (#33602) Fix names, deprecate duplicate, and make LinearMap.mul{Left, Right} extend AddMonoidHom.mul{Left, Right}. Follow up to #33405.

Estimated changes

Modified Mathlib/Algebra/Algebra/Bilinear.lean

deleted theorem LinearMap.toSpanSingleton_eq_algebra_linearMap

modified theorem LinearMap.toSpanSingleton_one_eq_algebraLinearMap

Modified Mathlib/Algebra/Algebra/Operations.lean

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

modified theorem LinearMap.mulLeft_one

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

deleted theorem LinearMap.mulLeft_toAddMonoidHom

modified theorem LinearMap.mulLeft_zero_eq_zero

deleted theorem LinearMap.mulRight_toAddMonoidHom

modified theorem LinearMap.mulRight_zero_eq_zero

added theorem LinearMap.toAddMonoidHom_mulLeft

added theorem LinearMap.toAddMonoidHom_mulRight