Theorem LinearMap.toSpanSingleton_eq_algebra_linearMap

Modification history

2024-10-26 13:22
Mathlib/Algebra/Algebra/Bilinear.lean
refactor: change the definition of `1 : Submodule R A` to the range of `(· • 1)` (#18092) …
Added LinearMap.toSpanSingleton_eq_algebra_linearMapView on Github →