Theorem LinearMap.toSpanSingleton_eq_algebra_linearMap

Modification history

2026-01-06 19:16
Mathlib/Algebra/Algebra/Bilinear.lean
chore(Algebra): some cleanup (#33602) …
Deleted LinearMap.toSpanSingleton_eq_algebra_linearMapView on Github →
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 →