Theorem max_aleph0_card_le_rank_fun_nat
Modification history
2024-12-09 12:57
Mathlib/LinearAlgebra/Dimension/DivisionRing.lean
chore: don't need group-theoretic exponent to set up finite dimensional vector spaces (#19827)
Modified max_aleph0_card_le_rank_fun_natView on Github →