mathlib3

2bca4d61 - chore(set_theory/ordinal/cantor_normal_form): mark `CNF` as `pp_nodot` (#15228)

chore(set_theory/ordinal/cantor_normal_form): mark `CNF` as `pp_nodot` (#15228) `b.CNF o` doesn't make much sense, since `b` is the base argument rather than the main argument. The existing lemmas all use the `CNF b o` spelling anyway.