Commit 2022-12-08 18:41 40494fe7

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.