refactor(SetTheory/Ordinal): redefine Ordinal.ToType as Shrink (Iio o) - #42925

refactor(SetTheory/Ordinal): redefine Ordinal.ToType as Shrink (Iio o)#42925

dennj wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

dennj:ordinal-totype-shrinkdennj/mathlib4:ordinal-totype-shrinkCopy head branch name to clipboard