sum_Icc_mu_right — Mathlib

English

Möbius function respects order duality: μ in αᵒᵈ relates to μ in α by μ_αᵒᵈ(a,b) = μ_α(b,a).

Русский

Функция Мёбиуса сохраняется при переходе к порядку-полуобратному: μ_{αᵒᵈ}(a,b) = μ_{α}(b,a).

LaTeX

$$$ μ 𝕜 (toDual a) (toDual b) = μ 𝕜 b a $$$

Lean4

theorem sum_Icc_mu_right (a b : α) : ∑ x ∈ Icc a b, mu 𝕜 a x = if a = b then 1 else 0 :=
  by
  split_ifs with hab
  · simp [hab]
  by_cases hab : a ≤ b
  · simp [Icc_eq_cons_Ico hab, mu_eq_neg_sum_Ico_of_ne ‹_›]
  · exact sum_eq_zero fun x hx ↦ apply_eq_zero_of_not_le (fun hax ↦ hab <| hax.trans (mem_Icc.1 hx).2) _

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