filter_coprime_Ico_eq_totient — Mathlib

English

For a, n, the number of x in Ico(k, k+n) coprime to a is φ(a) when counting in a consecutive block of length a.

Русский

Для любых a, k, n число x в Ico(k, k+n), таких что a и x взаимно просты, равно φ(a).

LaTeX

$$$$\#\{x ∈ \mathrm{Ico}(k, k+n) : a\perp x\} = φ(a).$$$$

Lean4

theorem filter_coprime_Ico_eq_totient (a n : ℕ) : #({x ∈ Ico n (n + a) | a.Coprime x}) = totient a :=
  by
  rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range]
  exact periodic_coprime a

Похожие утверждения