Theorem affineSpan_range_ne_top_of_card_le_finrank

Modification history

2026-09-11 08:52
Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
feat(LinearAlgebra/AffineSpace): show small finite families have proper affine span (#43469)
Added affineSpan_range_ne_top_of_card_le_finrankView on Github →