mathlib
bb90598b - feat(set_theory/ordinal/basic): Turn various lemmas into `simp` (#14075)

Commit

3 years ago

feat(set_theory/ordinal/basic): Turn various lemmas into `simp` (#14075)

Author

vihdzp

vihdzp

Parents

Loading