mathlib

2751ae21 - refactor(set_theory/ordinal/arithmetic): fix `rank` universes (#18239)

refactor(set_theory/ordinal/arithmetic): fix `rank` universes (#18239) The rank of an object in universe `u` should also be an ordinal in universe `u`, rather than universe `max u v` for some other `v`, as `ordinal.lift` can achieve this effect.