Theorem rank_dual_eq_card_dual_of_aleph0_le_rank'
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 rank_dual_eq_card_dual_of_aleph0_le_rank'View on Github →