Commit 2026-06-02 18:08 f3cf757a

View on Github →

chore: deprecate Nat.strongRec(On)' (#36165) In favour of Batteries's Nat.strongRec for definitions and Nat.strong_induction_on for proofs.

Estimated changes

Modified Mathlib/Analysis/Analytic/Inverse.lean

Modified Mathlib/Data/Int/GCD.lean

modified theorem Nat.gcdA_zero_left

modified theorem Nat.gcdB_zero_left

modified theorem Nat.xgcd_zero_left

Modified Mathlib/Data/Nat/Factorization/Induction.lean

Modified Mathlib/Data/Nat/Init.lean

deleted theorem Nat.strongRec'_spec

deleted def Nat.strongRecOn'

deleted theorem Nat.strongRecOn'_beta

Modified Mathlib/Data/Set/Finite/Basic.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/Topology/EMetricSpace/Paracompact.lean

Modified MathlibTest/EllipticCurve.lean