Theorem MvPolynomial.cardinalMk_le_max_lift

Modification history

2026-03-26 09:32
Mathlib/Algebra/MvPolynomial/Cardinal.lean
refactor(Algebra/MvPolynomial): turn into an `abbrev` (#36678) …
Modified MvPolynomial.cardinalMk_le_max_liftView on Github →
2024-11-23 04:58
Mathlib/Algebra/MvPolynomial/Cardinal.lean
feat: add `(Algebra|IntermediateField).lift_cardinalMk_adjoin_le` (#19327) …
Added MvPolynomial.cardinalMk_le_max_liftView on Github →