Theorem affineSpan_eq_top_iff_nonempty_of_subsingleton

Modification history

2025-07-06 23:41
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
feat(LinearAlgebra/AffineSpace): lemmas for trivial spaces (#26821) …
Added affineSpan_eq_top_iff_nonempty_of_subsingletonView on Github →