Theorem Finset.range_subset_range

Modification history

2025-09-16 09:16
Mathlib/Data/Finset/Range.lean
feat: grind annotations for Finset.range (#29426)
Modified Finset.range_subset_rangeView on Github →
2025-09-11 00:00
Mathlib/Data/Finset/Range.lean
chore(Data/Finset): deprecate `range_succ`; rename `range_subset` to `range_subset_range` (#29509) …
Added Finset.range_subset_rangeView on Github →