Counting elements in an interval with given residue #
The theorems in this file generalise Nat.card_multiples in Mathlib.Data.Nat.Factorization.Basic
to all integer intervals and any fixed residue (not just zero, which reduces to the multiples).
Theorems are given for Ico and Ioc intervals.
theorem
Int.Ico_filter_modEq_eq
(a b : ℤ)
{r : ℤ}
(v : ℤ)
:
{x ∈ Finset.Ico a b | x ≡ v [ZMOD r]} = Finset.map { toFun := fun (x : ℤ) => x + v, inj' := ⋯ } ({x ∈ Finset.Ico (a - v) (b - v) | r ∣ x})
theorem
Int.Ioc_filter_modEq_eq
(a b : ℤ)
{r : ℤ}
(v : ℤ)
:
{x ∈ Finset.Ioc a b | x ≡ v [ZMOD r]} = Finset.map { toFun := fun (x : ℤ) => x + v, inj' := ⋯ } ({x ∈ Finset.Ioc (a - v) (b - v) | r ∣ x})
theorem
Int.Ico_filter_dvd_eq
(a b : ℤ)
{r : ℤ}
(hr : 0 < r)
:
{x ∈ Finset.Ico a b | r ∣ x} = Finset.map { toFun := fun (x : ℤ) => x * r, inj' := ⋯ } (Finset.Ico ⌈↑a / ↑r⌉ ⌈↑b / ↑r⌉)
theorem
Int.Ioc_filter_dvd_eq
(a b : ℤ)
{r : ℤ}
(hr : 0 < r)
:
{x ∈ Finset.Ioc a b | r ∣ x} = Finset.map { toFun := fun (x : ℤ) => x * r, inj' := ⋯ } (Finset.Ioc ⌊↑a / ↑r⌋ ⌊↑b / ↑r⌋)
theorem
Nat.Ico_filter_modEq_cast
(a b : ℕ)
{r v : ℕ}
:
Finset.map castEmbedding ({x ∈ Finset.Ico a b | x ≡ v [MOD r]}) = {x ∈ Finset.Ico ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}
theorem
Nat.Ioc_filter_modEq_cast
(a b : ℕ)
{r v : ℕ}
:
Finset.map castEmbedding ({x ∈ Finset.Ioc a b | x ≡ v [MOD r]}) = {x ∈ Finset.Ioc ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}