Theorem Module.Projective.exists_dual_ne_zero

Modification history

2025-12-08 18:59
Mathlib/LinearAlgebra/Dual/Lemmas.lean
feat(LinearAlgebra/GeneralLinearGroup): algebra automorphisms in endomorphisms are inner (#28100) …
Added Module.Projective.exists_dual_ne_zeroView on Github →