Def Nat.decreasingInduction'

Modification history

2024-04-07 07:06

Mathlib/Data/Nat/Defs.lean

chore: Split `Data.{Nat,Int}{.Order}.Basic` in group vs ring instances (#11924) …

Modified Nat.decreasingInduction'View on Github →

2024-01-10 08:02

Mathlib/Data/Nat/Basic.lean

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

Modified Nat.decreasingInduction'View on Github →

2023-08-10 19:52

Mathlib/Data/Nat/Basic.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Nat.decreasingInduction'View on Github →

2022-11-30 18:00

Mathlib/Data/Nat/Basic.lean

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

Added Nat.decreasingInduction'View on Github →