Commit 2026-01-05 09:39 d679c86f

View on Github →

feat: range of Finsupp is finite (#33530)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Basic.lean

added theorem Polynomial.finite_range_coeff

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.finite_range

modified theorem Finsupp.frange_single

modified theorem Finsupp.mem_frange

added theorem Finsupp.mem_frange_of_mem

added theorem Finsupp.range_subset_insert_frange