Commit 2025-08-29 07:32 aaabaed3

View on Github →

chore: fix more induction/recursor branch names (#25770) These were found using the regex \| h. => and def.*rec.*\(h. :.

Estimated changes

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Data/ENat/Basic.lean

modified theorem ENat.nat_induction

Modified Mathlib/Data/Fin/Tuple/Basic.lean

modified def Fin.consInduction

Modified Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean

Modified Mathlib/Data/Seq/Computation.lean

modified def Computation.recOn

Modified Mathlib/Data/Set/Card.lean

Modified Mathlib/Data/WSeq/Basic.lean

modified def Stream'.WSeq.recOn

Modified Mathlib/Logic/Function/Iterate.lean

modified def Function.Iterate.rec

modified theorem Function.Iterate.rec_zero

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

Modified Mathlib/Order/SuccPred/Archimedean.lean

Modified Mathlib/Order/Synonym.lean