Commit 2026-09-30 17:48 0d149aa7

feat(LinearAlgebra/Dimension/Constructions): Set.ncard version of four lemmas (#44359) Four lemmas here have hypotheses (s : Set M) [Fintype s] and mention s.toFinset.card. We add Set.ncard versions for them. finrank_span_set_eq_ncard does not even need finiteness, which leads to a shorter proof of finrank_span_set_eq_card.