Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-04 16:01 1cc59b9d

View on Github →

feat(set_theory/cardinal, data/nat/fincard): Define nat- and enat-valued cardinalities (#6494) Defines cardinal.to_nat and cardinal.to_enat Uses those to define nat.card and enat.card

Estimated changes

Modified src/linear_algebra/finite_dimensional.lean

Modified src/set_theory/cardinal.lean

added theorem cardinal.cast_to_nat_of_lt_omega

added theorem cardinal.mk_to_enat_eq_coe_card

added theorem cardinal.mk_to_enat_of_infinite

added theorem cardinal.mk_to_nat_eq_card

added theorem cardinal.mk_to_nat_of_infinite

added theorem cardinal.one_to_nat

added theorem cardinal.to_enat_apply_of_lt_omega

added theorem cardinal.to_enat_apply_of_omega_le

added theorem cardinal.to_enat_cast

added theorem cardinal.to_enat_surjective

added theorem cardinal.to_nat_apply_of_lt_omega

added theorem cardinal.to_nat_apply_of_omega_le

added theorem cardinal.to_nat_cast

added theorem cardinal.to_nat_right_inverse

added theorem cardinal.to_nat_surjective

added theorem cardinal.zero_to_nat