Theorem finrank_span_le_ncard

Modification history

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