Theorem LinearMap.id_separatingLeft

Modification history

2026-08-31 20:31
Mathlib/LinearAlgebra/Dual/Lemmas.lean
feat(LinearAlgebra/SesquilinearForm): add basic lemmas for bilinear forms (#34487) …
Deleted LinearMap.id_separatingLeftView on Github →
2026-04-28 19:12
Mathlib/LinearAlgebra/Dual/Lemmas.lean
chore(LinearAlgebra/Dual): deprecate `Module.dualPairing` (#37542) …
Added LinearMap.id_separatingLeftView on Github →