moebius_ne_zero_iff_squarefree

Mathlib.NumberTheory.ArithmeticFunction

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

English

μ(n) ≠ 0 iff μ(n) ∈ {1, -1}.

Русский

μ(n) ≠ 0 тогда и только тогда, когда μ(n) ∈ {1, -1}.

LaTeX

$$μ(n) ≠ 0 ⇔ μ(n) = 1 ∨ μ(n) = -1$$

Lean4

theorem moebius_ne_zero_iff_squarefree {n : ℕ} : μ n ≠ 0 ↔ Squarefree n :=
  by
  constructor <;> intro h
  · contrapose! h
    simp [h]
  · simp [h]

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

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

Разделы

Аффилиация

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