Def Nat.twoStepInduction

Modification history

2024-09-02 23:30

Mathlib/Data/Nat/Defs.lean

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

Modified Nat.twoStepInduction View on Github →

2023-07-10 13:59

Mathlib/Init/Data/Nat/Lemmas.lean

feat: port Init.Data.Nat.Lemmas (#5782) …

Added Nat.twoStepInduction View on Github →