mathlib

c5267895 - feat(set_theory/ordinal_arithmetic): `is_normal.eq_iff_zero_and_succ` (#12222)

feat(set_theory/ordinal_arithmetic): `is_normal.eq_iff_zero_and_succ` (#12222) Two normal functions are equal iff they're equal at `0` and successor ordinals. This is used for a few lemmas in #12202.