coe_zeta_mul_moebius

Mathlib.NumberTheory.ArithmeticFunction

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

English

μ(n)^2 = 1 if Squarefree(n) else 0.

Русский

μ(n)^2 = 1, если n квадратноразложимо, иначе 0.

LaTeX

$$μ(n)^2 = if Squarefree(n) then 1 else 0$$

Lean4

@[simp]
theorem coe_zeta_mul_moebius : (ζ * μ : ArithmeticFunction ℤ) = 1 := by rw [mul_comm, moebius_mul_coe_zeta]

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

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

Разделы

Аффилиация

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