Commit 2024-11-23 04:58 8d7c6def

View on Github →

feat: add (Algebra|IntermediateField).lift_cardinalMk_adjoin_le (#19327) Also add FreeAlgebra.cardinalMk_eq_max_lift, etc. parallel to MvPolynomial. Also fix the name cardinal_lift_mk_le_max -> cardinalMk_le_max_lift for MvPolynomial.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/FreeAlgebra/Cardinality.lean

added theorem Algebra.cardinalMk_adjoin_le

added theorem Algebra.lift_cardinalMk_adjoin_le

added theorem FreeAlgebra.cardinalMk_eq

added theorem FreeAlgebra.cardinalMk_eq_lift

added theorem FreeAlgebra.cardinalMk_eq_max

added theorem FreeAlgebra.cardinalMk_eq_max_lift

added theorem FreeAlgebra.cardinalMk_eq_one

added theorem FreeAlgebra.cardinalMk_le_max

added theorem FreeAlgebra.cardinalMk_le_max_lift

Modified Mathlib/Algebra/MvPolynomial/Cardinal.lean

added theorem MvPolynomial.cardinalMk_eq

added theorem MvPolynomial.cardinalMk_eq_one

added theorem MvPolynomial.cardinalMk_le_max_lift

deleted theorem MvPolynomial.cardinal_lift_mk_le_max

Modified Mathlib/FieldTheory/Adjoin.lean

added theorem IntermediateField.cardinalMk_adjoin_le

added theorem IntermediateField.lift_cardinalMk_adjoin_le