mathlib3

4cdde79f - chore(set_theory/game/ordinal): minor golfing (#14317)

chore(set_theory/game/ordinal): minor golfing (#14317) We open the `pgame` namespace to save a few characters. We also very slightly golf the proof of `to_pgame_le`.