mathlib3
31b269b6 - feat(set_theory/ordinal/natural_ops): define natural multiplication (#14324)

Commit

2 years ago

feat(set_theory/ordinal/natural_ops): define natural multiplication (#14324)

Author

vihdzp

vihdzp

Parents

Loading