Theorem MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite'

Modification history

2026-03-26 09:32
Mathlib/Algebra/MonoidAlgebra/Cardinal.lean
refactor(Algebra/MvPolynomial): turn into an `abbrev` (#36678) …
Added MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite'View on Github →