moebius_eq_zero_of_not_squarefree

Mathlib.NumberTheory.ArithmeticFunction

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

English

If n is not squarefree, then μ(n) = 0.

Русский

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

LaTeX

$$¬\text{Squarefree}(n) ⇒ μ(n) = 0$$

Lean4

@[simp]
theorem moebius_eq_zero_of_not_squarefree {n : ℕ} (h : ¬Squarefree n) : μ n = 0 :=
  if_neg h

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

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

Разделы

Аффилиация

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