Theorem Module.Dual.range_eq_top_of_ne_zero

Modification history

2025-09-27 10:18
Mathlib/LinearAlgebra/Dual/Lemmas.lean
feat(Algebra/Module/LinearMap): `range (f.smulRight x) = span {x}` (#28350)
Modified Module.Dual.range_eq_top_of_ne_zeroView on Github →
2024-04-20 13:53
Mathlib/LinearAlgebra/Dual.lean
feat: define the coroots of a semisimple Lie algebra (#10893) …
Added Module.Dual.range_eq_top_of_ne_zeroView on Github →