Theorem Nat.findGreatest_pos

Modification history

2024-07-16 00:30

Mathlib/Data/Nat/Defs.lean

chore: move Nat.find/findGreatest into their own file (#11891) …

Modified Nat.findGreatest_pos View on Github →

2024-03-26 23:09

Mathlib/Data/Nat/Defs.lean

chore(Data/Nat): Use Std lemmas (#11661) …

Modified Nat.findGreatest_pos View on Github →

2023-09-22 08:17

Mathlib/Data/Nat/Order/Basic.lean

feat: Zeckendorf's theorem (#6880) …

Added Nat.findGreatest_pos View on Github →