Commit 2025-08-22 20:53 8aca3483

View on Github →

chore(Data/Nat): deprecate exists_lt_succ (duplicate) (#28456)

Estimated changes

Modified Mathlib/Data/List/Range.lean

Modified Mathlib/Data/Nat/Init.lean

deleted theorem Nat.exists_lt_succ

deleted theorem Nat.forall_lt_succ