mathlib3
ccf646d3 - chore(set_theory/ordinal): use a `protected lemma` to drop a `nolint` (#2805)

Commit

5 years ago

chore(set_theory/ordinal): use a `protected lemma` to drop a `nolint` (#2805)

Author

urkud

urkud

Parents

Loading