Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-04 18:18 28592d99

View on Github →

feat(set_theory/cardinal): cardinal.to_nat_mul (#8943) cardinal.to_nat distributes over multiplication.

Estimated changes

Modified src/set_theory/cardinal.lean

added theorem cardinal.cast_to_nat_of_omega_le

added theorem cardinal.nat_cast_injective

added theorem cardinal.to_nat_mul