Commit 2026-03-15 10:57 b12200df

View on Github →

chore(SetTheory/Ordinal): deprecate more theorems on succ (#35853) The idea is that we should simply write x + 1 instead of succ x.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

modified theorem Cardinal.isSuccLimit_ord

Modified Mathlib/SetTheory/Ordinal/Basic.lean

added theorem Ordinal.card_add_one

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/FixedPoint.lean

Modified Mathlib/SetTheory/Ordinal/Notation.lean

Modified Mathlib/SetTheory/Ordinal/Principal.lean

Modified Mathlib/SetTheory/Ordinal/Topology.lean