one_smul' — Mathlib

English

The zeta function on arithmetic functions ℕ is defined by ζ(0) = 0 and ζ(x) = 1 for x > 0.

Русский

Функция дзета на арифметических функциях ℕ задана как ζ(0) = 0 и ζ(x) = 1 для x > 0.

LaTeX

$$$\\zeta:\\mathbb{N} \\to \\mathbb{N}, \\quad \\zeta(n) = \\begin{cases}0, & n=0, \\\\ 1, & n>0.\\end{cases}$$$

Lean4

theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b :=
  by
  ext x
  rw [smul_apply]
  by_cases x0 : x = 0
  · simp [x0]
  have h : {(1, x)} ⊆ divisorsAntidiagonal x := by simp [x0]
  rw [← sum_subset h]
  · simp
  intro y ymem ynotMem
  have y1ne : y.fst ≠ 1 := fun con => by simp_all [Prod.ext_iff]
  simp [y1ne]

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