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