Commit 2023-03-26 18:06 780abda6

View on Github →

feat: port Data.MvPolynomial.Cardinal (#3090)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MvPolynomial/Cardinal.lean

added theorem MvPolynomial.cardinal_lift_mk_le_max

added theorem MvPolynomial.cardinal_mk_eq_lift

added theorem MvPolynomial.cardinal_mk_eq_max

added theorem MvPolynomial.cardinal_mk_eq_max_lift

added theorem MvPolynomial.cardinal_mk_le_max