mathlib3
c030dd2a - feat(set_theory/cardinal): `cardinal.to_nat` is order-preserving on finite cardinals (#12763)
Commit
View On GitHub
Commit
3 years ago
feat(set_theory/cardinal): `cardinal.to_nat` is order-preserving on finite cardinals (#12763) This PR proves that `cardinal.to_nat` is order-preserving on finite cardinals.
Author
tb65536 tb65536
Parents
2873b7ac
FAQ Terms Privacy Refunds Impressum
Loading