pow_apply

Mathlib.Algebra.Module.LinearMap.End

URI: https://scilib.ai/kg/mathlib#Module.End.pow_apply

English

For every n, and every m in M, (f^n)(m) = f^{[n]}(m); the nth power acts the same as the nth iterate on elements.

Русский

Для каждого n и каждого m ∈ M верно: (f^n)(m) = f^{[n]}(m).

LaTeX

$$$\\forall m\\in M,\\; (f^n)(m) = f^{[n]}(m).$$$

Lean4

theorem pow_apply (f : End R M) (n : ℕ) (m : M) : (f ^ n) m = f^[n] m :=
  congr_fun (coe_pow f n) m

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

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

Разделы

Аффилиация

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