Commit 2025-08-08 10:54 6a8a98db

View on Github →

feat(Algebra/Algebra/Bilinear): mulLeft_inj and mulRight_inj (#27999)

Estimated changes

Modified Mathlib/Algebra/Algebra/Bilinear.lean

modified theorem LinearMap.mulLeft_eq_zero_iff

added theorem LinearMap.mulLeft_inj

modified theorem LinearMap.mulRight_eq_zero_iff

added theorem LinearMap.mulRight_inj