Theorem Module.Basis.setFinite_index_of_rank_lt_aleph0

Modification history

2026-10-13 18:03
Mathlib/LinearAlgebra/Dimension/Finite.lean
chore: remove `Nonempty (Fintype _)` (#44764) …
Added Module.Basis.setFinite_index_of_rank_lt_aleph0View on Github →