Commit 2023-03-02 17:41 591e208d

View on Github →

chore: swap the names of InitialSeg.init and InitialSeg.init' (#2581) mathlib3 PR: https://github.com/leanprover-community/mathlib/pull/18534

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

deleted theorem InitialSeg.init'

added theorem InitialSeg.init

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean