Commit 2024-09-02 23:30 4bb220d4

View on Github →

chore: deprecate Init.Data.Nat.Lemmas (#16096)

Estimated changes

Modified Archive/Arithcc.lean

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Algebra/Order/Ring/Nat.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/Nat/Defs.lean

added def Nat.twoStepInduction

Modified Mathlib/Data/Nat/Dist.lean

Modified Mathlib/Data/Nat/Fib/Basic.lean

Modified Mathlib/Data/Nat/GCD/Basic.lean

Modified Mathlib/Data/Nat/Log.lean

Modified Mathlib/Init/Data/Nat/Lemmas.lean

deleted theorem Nat.eq_zero_of_mul_eq_zero

deleted def Nat.twoStepInduction

Modified Mathlib/Order/Defs.lean

Modified Mathlib/Order/Fin/Basic.lean

Modified test/ExtractGoal.lean

Modified test/MoveAdd.lean

Modified test/byContra.lean

Modified test/notation3.lean