mathlib

40494fe7 - feat(algebra/algebraic_card): prove `algebraic.cardinal_mk_lift_of_infinite` (#17742)

feat(algebra/algebraic_card): prove `algebraic.cardinal_mk_lift_of_infinite` (#17742) * Add `cardinal.mul_le_max_of_aleph_0_le_right` and `cardinal.lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le`. * Add `algebraic.infinite_of_char_zero`. * Golf `algebraic.cardinal_mk_lift_le_mul` by moving some lemmas to `cardinal.*`. * Upgrade `algebraic.cardinal_mk_lift_le_of_infinite` to `algebraic.cardinal_mk_lift_of_infinite`. * Upgrade `algebraic.cardinal_mk_le_of_infinite` to `algebraic.cardinal_mk_of_infinite`. * Rename `algebraic.countable_of_encodable` to `algebraic.countable`, assume `[countable R]` instead of `[encodable R]`. * Rename `algebraic.cardinal_mk_of_encodable_of_char_zero` to `algebraic.cardinal_mk_of_countble_of_char_zero`.