Theorem finrank_span_set_eq_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_set_eq_ncardView on Github →