Commit 2025-09-16 09:16 ec636b97

View on Github →

feat: grind annotations for Finset.range (#29426)

Estimated changes

Modified Mathlib/Data/Finset/Empty.lean

added theorem Finset.nonempty_def

Modified Mathlib/Data/Finset/Range.lean

modified theorem Finset.mem_range_le

modified theorem Finset.mem_range_sub_ne_zero

modified theorem Finset.mem_range_succ_iff

modified theorem Finset.notMem_range_self

modified theorem Finset.range_add_one

modified theorem Finset.range_subset_range

modified theorem Finset.self_mem_range_succ