Commit 2026-10-13 18:03 fcd79238

View on Github →

chore: remove Nonempty (Fintype _) (#44764) Change a theorem statement to not say Nonempty (Fintype _), and instead conclude Finite _.

Estimated changes

Modified Mathlib/FieldTheory/Finiteness.lean

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

Modified Mathlib/LinearAlgebra/Dimension/Finite.lean

modified theorem Module.Basis.finite_index_of_rank_lt_aleph0

added theorem Module.Basis.setFinite_index_of_rank_lt_aleph0