isMultiplicative_zeta

Mathlib.NumberTheory.ArithmeticFunction

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.isMultiplicative_zeta

English

The zeta function is multiplicative: for coprime m,n, ζ(mn) = ζ(m) ζ(n).

Русский

Функция дзета мультипликативна: для взаимно простых m,n выполняется ζ(mn) = ζ(m) ζ(n).

LaTeX

$$$ \zeta(mn) = \zeta(m) \zeta(n) $$$

Lean4

@[arith_mult]
theorem isMultiplicative_zeta : IsMultiplicative ζ :=
  IsMultiplicative.iff_ne_zero.2 ⟨by simp, by simp +contextual⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru