Def Nat.iterate

Modification history

2023-09-06 22:20

Mathlib/Init/Data/Nat/Lemmas.lean

chore: cleanup in Mathlib.Init (#6977)

Modified Nat.iterate View on Github →

2021-09-29 16:59

Mathlib/Init/Data/Nat/Lemmas.lean

feat: add Init/Data/Nat/Basic.lean and Init/Data/Nat/Lemmas.lean (#48) …

Added Nat.iterate View on Github →