Theorems · Theorem · order theory

Nat.image_Ico_mod

∀ (n a : ℕ), Finset.image (fun x => x % a) (Finset.Ico n (n + a)) = Finset.range a

Note that while this lemma cannot be easily generalized to a type class, it holds for ℤ as well. See Int.image_Ico_emod for the ℤ version.

Defined in

Mathlib.Order.Interval.Finset.Nat

Cited by

1 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound