abs_moebius

Mathlib.NumberTheory.ArithmeticFunction

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem abs_moebius {n : ℕ} : |μ n| = if Squarefree n then 1 else 0 :=
  by
  split_ifs with h
  · exact abs_moebius_eq_one_of_squarefree h
  · simp only [moebius_eq_zero_of_not_squarefree h, abs_zero]

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

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

Разделы

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

Аффилиация

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