mathlib3
28592d99 - feat(set_theory/cardinal): cardinal.to_nat_mul (#8943)

Commit

4 years ago

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

Author

tb65536

Parents