Theorem span_lt_of_subset_of_ncard_lt_finrank

Modification history

2026-09-30 17:48
Mathlib/LinearAlgebra/Dimension/Constructions.lean
feat(LinearAlgebra/Dimension/Constructions): `Set.ncard` version of four lemmas (#44359) …
Added span_lt_of_subset_of_ncard_lt_finrankView on Github →