Commit 2026-02-03 17:15 6f699a95

View on Github →

feat: (Multiset.range n).toFinset = .range n (#34681) From ClassFieldTheory

Estimated changes

Modified Mathlib/Data/Finset/Range.lean

added theorem Multiset.toFinset_range