Theorem Cardinal.mk_le_mk_mul_of_mk_preimage_le

Modification history