Commit 2026-01-05 14:32 d1446af9

View on Github →

chore(Algebra): move LinearMap.mul{Left, Right, LeftRight} to earlier file (#33405) No code changed: literally just move.

Estimated changes

Modified Mathlib/Algebra/Algebra/Bilinear.lean

deleted def LinearMap.mulLeft

deleted def LinearMap.mulLeftRight

deleted theorem LinearMap.mulLeftRight_apply

deleted theorem LinearMap.mulLeft_apply

deleted theorem LinearMap.mulLeft_eq_zero_iff

deleted theorem LinearMap.mulLeft_inj

deleted theorem LinearMap.mulLeft_mul

deleted theorem LinearMap.mulLeft_one

deleted theorem LinearMap.mulLeft_toAddMonoidHom

deleted theorem LinearMap.mulLeft_zero_eq_zero

deleted def LinearMap.mulRight

deleted theorem LinearMap.mulRight_apply

deleted theorem LinearMap.mulRight_eq_zero_iff

deleted theorem LinearMap.mulRight_inj

deleted theorem LinearMap.mulRight_mul

deleted theorem LinearMap.mulRight_one

deleted theorem LinearMap.mulRight_toAddMonoidHom

deleted theorem LinearMap.mulRight_zero_eq_zero

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

added theorem LinearMap.mulLeft_eq_zero_iff

added theorem LinearMap.mulLeft_inj

added theorem LinearMap.mulLeft_mul

added theorem LinearMap.mulLeft_one

added theorem LinearMap.mulRight_eq_zero_iff

added theorem LinearMap.mulRight_inj

added theorem LinearMap.mulRight_mul

added theorem LinearMap.mulRight_one

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

added def LinearMap.mulLeft

added def LinearMap.mulLeftRight

added theorem LinearMap.mulLeftRight_apply

added theorem LinearMap.mulLeft_apply

added theorem LinearMap.mulLeft_toAddMonoidHom

added theorem LinearMap.mulLeft_zero_eq_zero

added def LinearMap.mulRight

added theorem LinearMap.mulRight_apply

added theorem LinearMap.mulRight_toAddMonoidHom

added theorem LinearMap.mulRight_zero_eq_zero