pow_one_eq_id

Mathlib.NumberTheory.ArithmeticFunction

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

English

In the arithmetic-function monoid under pointwise multiplication, the first power of the identity function is the identity function itself.

Русский

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

LaTeX

$$$ \mathrm{pow}(1) = \mathrm{id} $$$

Lean4

theorem pow_one_eq_id : pow 1 = id := by
  ext n
  simp

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

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

Разделы

Аффилиация

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