[Merged by Bors] - chore: use notation3 for Ordinal.typeLT#39798

vihdzp wants to merge 2 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

vihdzp:typeltvihdzp/mathlib4:typeltCopy head branch name to clipboard