Commit 2023-07-20 00:27 876c8e0e

View on Github →

chore: golf set_theory/ordinal/basic (#5581)

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

added theorem PrincipalSeg.apply_subrelIso

added theorem PrincipalSeg.subrelIso_apply

Modified Mathlib/SetTheory/Ordinal/Basic.lean

modified def Ordinal.enum

modified def Ordinal.enumIso