coe_moebius_mul_coe_zeta

Mathlib.NumberTheory.ArithmeticFunction

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

← MathLib Explorer

English

abs μ(n) = if Squarefree(n) then 1 else 0.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coe_moebius_mul_coe_zeta [Ring R] : (μ * ζ : ArithmeticFunction R) = 1 := by
  rw [← coe_coe, ← intCoe_mul, moebius_mul_coe_zeta, intCoe_one]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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