mathlib

991ff3b5 - golf(set_theory/ordinal/cantor_normal_form): golf theorems (#16009)

golf(set_theory/ordinal/cantor_normal_form): golf theorems (#16009) We move `div_opow_log_pos` out of a proof and open the `list` namespace. Mathlib 4: https://github.com/leanprover-community/mathlib4/pull/3189