Commit 2025-04-11 21:03 e2bc6a06

View on Github →

chore: fix yet more induction branch names (#23686) Follow-up to #23448. This includes the entire stack of inductors in Order.SuccPred.Limit.

Estimated changes

Modified Mathlib/AlgebraicTopology/RelativeCellComplex/Basic.lean

Modified Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Monomorphisms.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Preorder/HasIterationOfShape.lean

Modified Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean

Modified Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean

Modified Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean

Modified Mathlib/CategoryTheory/SmallObject/WellOrderInductionData.lean

Modified Mathlib/Computability/TuringMachine.lean

modified def Turing.TM2to1.stmtStRec.{l}

Modified Mathlib/Order/DirectedInverseSystem.lean

Modified Mathlib/Order/IsNormal.lean

Modified Mathlib/Order/SuccPred/Limit.lean

modified theorem Order.isPredLimitRecOn_of_isMax

modified theorem Order.isPredLimitRecOn_pred_of_not_isMin

modified theorem Order.isPredPrelimitRecOn_pred_of_not_isMin

modified theorem Order.isSuccLimitRecOn_of_isMin

modified theorem Order.isSuccLimitRecOn_succ_of_not_isMax

modified theorem Order.isSuccPrelimitRecOn_succ_of_not_isMax

modified theorem PredOrder.limitRecOn_isMax

modified theorem PredOrder.limitRecOn_pred_of_not_isMin

modified theorem PredOrder.prelimitRecOn_pred_of_not_isMin

modified theorem SuccOrder.limitRecOn_isMin

modified theorem SuccOrder.limitRecOn_succ_of_not_isMax

modified theorem SuccOrder.prelimitRecOn_succ_of_not_isMax

Modified Mathlib/Order/TransfiniteIteration.lean

Modified Mathlib/RingTheory/IsTensorProduct.lean

modified theorem IsTensorProduct.inductionOn

Modified Mathlib/RingTheory/Kaehler/TensorProduct.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

modified def Ordinal.boundedLimitRecOn

modified theorem Ordinal.boundedLimitRec_limit

modified theorem Ordinal.boundedLimitRec_succ

modified theorem Ordinal.boundedLimitRec_zero

modified def Ordinal.limitRecOn

modified theorem Ordinal.limitRecOn_limit

modified theorem Ordinal.limitRecOn_succ

modified theorem Ordinal.limitRecOn_zero

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified Mathlib/SetTheory/Ordinal/Family.lean

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean