Commit 2025-09-06 05:41 9e3250f9

View on Github →

feat: PosMulStrictMono Ordinal (#28943) We also deprecate various theorems that were just stating corollaries of this typeclass.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Ordinal.mul_ne_zero

deleted theorem Ordinal.mul_pos

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean