Def Nat.leRecOn

Modification history

2024-07-13 07:32

Mathlib/Data/Nat/Defs.lean

feat: a replacement for `Nat.leRecOn'` that works with `induction` (#14431) …

Modified Nat.leRecOn View on Github →

2024-01-10 08:02

Mathlib/Data/Nat/Basic.lean

refactor: Split off basic `Nat` file (#9551) …

Modified Nat.leRecOn View on Github →

2022-11-30 18:00

Mathlib/Data/Nat/Basic.lean

feat: port Data.Nat.Basic (#729) …

Added Nat.leRecOn View on Github →