pow_apply — Mathlib

English

There is a natural power structure on OneHom M N turning it into a monoid under exponentiation by natural numbers.

Русский

Существует естественная структура возведения в степень на OneHom M N, которая превращает его в моноид по степеням натуральных чисел.

LaTeX

$$$\text{Pow }(\mathrm{OneHom}\,M\,N)\;\text{Nat}$$$

Lean4

@[to_additive (attr := simp)]
theorem pow_apply [MulOneClass M] [CommMonoid N] (f : M →* N) (n : ℕ) (x : M) : (f ^ n) x = f x ^ n :=
  rfl

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