Commit 2023-07-17 07:06 f49a8091

View on Github →

chore: partial forward port of 14324 (#5954) This doesn't yet forward port the changes to Mathlib/SetTheory/Ordinal/NaturalOps.lean.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

added def Ordinal.blsub₂

added theorem Ordinal.lt_blsub₂

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

deleted def Ordinal.blsub₂

deleted theorem Ordinal.lt_blsub₂