Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-09-11 08:52
fa30f281
View on Github →
feat(LinearAlgebra/AffineSpace): show small finite families have proper affine span (
#43469
)
Estimated changes
Modified
Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
added
theorem
affineSpan_image_ne_top_of_encard_le_finrank
added
theorem
affineSpan_range_ne_top_of_card_le_finrank