Commit 2023-05-22 22:00 5afb4f38

View on Github →

feat: port Algebra.AlgebraicCard (#4236)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/AlgebraicCard.lean

added theorem Algebraic.aleph0_le_cardinal_mk_of_charZero

added theorem Algebraic.cardinal_mk_le_max

added theorem Algebraic.cardinal_mk_le_mul

added theorem Algebraic.cardinal_mk_lift_le_max

added theorem Algebraic.cardinal_mk_lift_le_mul

added theorem Algebraic.cardinal_mk_lift_of_infinite

added theorem Algebraic.cardinal_mk_of_countble_of_charZero

added theorem Algebraic.cardinal_mk_of_infinite

added theorem Algebraic.infinite_of_charZero