pow_zero_eq_zeta — Mathlib

English

In the monoid of arithmetic functions under pointwise multiplication, the zero-th power equals the constant-one function, i.e., pow 0 = ζ.

Русский

В моноиде арифметических функций по точечному умножению нулевая степень равна константной единичной функции ζ; то есть pow 0 = ζ.

LaTeX

$$$ \mathrm{pow}(0) = \zeta $$$

Lean4

theorem pow_zero_eq_zeta : pow 0 = ζ := by
  ext n
  simp

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