Theorem Algebra.IsAlgebraic.lift_cardinalMk_le_max

Modification history

2024-11-28 12:19
Mathlib/RingTheory/Algebraic/Cardinality.lean
feat: `IntermediateField.rank_sup_le` (#19527) …
Added Algebra.IsAlgebraic.lift_cardinalMk_le_maxView on Github →