Theorem Finset.nonempty_range_succ
Modification history
2025-09-11 00:00
Mathlib/Data/Finset/Range.lean
chore(Data/Finset): deprecate `range_succ`; rename `range_subset` to `range_subset_range` (#29509) …
Deleted Finset.nonempty_range_succView on Github →2024-11-11 13:54
Mathlib/Data/Finset/Range.lean
chore(Data/Finset): split `Basic.lean` into many smaller files (#18610) …
Added Finset.nonempty_range_succView on Github →