instInhabited

Mathlib.Algebra.Group.Hom.Defs

URI: https://scilib.ai/kg/mathlib#Monoid.End.instInhabited

English

For f in End(M) and n in N, the function corresponding to f^n equals the n-th iterate of f: ↑(f^n) = f^[n].

Русский

Для f ∈ End(M) и n ∈ ℕ соответствующая функция к f^n равна n-й итерации функции f: ↑(f^n) = f^[n].

LaTeX

$$$\\forall f\\in \\operatorname{End}(M),\\; \\forall n\\in \\mathbb{N},\\quad \\uparrow(f^n)=f^{[n]}.$$$

Lean4

@[to_additive]
instance : Inhabited (Monoid.End M) :=
  ⟨1⟩

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

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

Разделы

Аффилиация

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