Def LinearMap.mulLeft

Modification history

2024-12-01 01:39

Mathlib/Algebra/Algebra/Bilinear.lean

refactor(Algebra/Bilinear): generalize to non-commutative base rings (#19232) …

Modified LinearMap.mulLeft View on Github →

2023-03-01 18:09

Mathlib/Algebra/Algebra/Bilinear.lean

feat: port Algebra.Algebra.Bilinear (#2552)

Added LinearMap.mulLeft View on Github →