moebius_sq

Mathlib.NumberTheory.ArithmeticFunction

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem moebius_sq {n : ℕ} : μ n ^ 2 = if Squarefree n then 1 else 0 :=
  by
  split_ifs with h
  · exact moebius_sq_eq_one_of_squarefree h
  · simp only [moebius_eq_zero_of_not_squarefree h, zero_pow (show 2 ≠ 0 by simp)]

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

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

Разделы

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

Аффилиация

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