iterate_map_one

Mathlib.Algebra.Group.Hom.Defs

URI: https://scilib.ai/kg/mathlib#iterate_map_one

← MathLib Explorer

English

Iterating a multiplicative endomorphism on the identity yields the identity: f^[n](1) = 1.

Русский

Итерация конечного эндоморфизма на единице даёт единицу: f^[n](1) = 1.

LaTeX

$$$f^{[n]}(1) = 1.$$$

Lean4

@[to_additive (attr := simp)]
theorem iterate_map_one {M F : Type*} [One M] [FunLike F M M] [OneHomClass F M M] (f : F) (n : ℕ) : f^[n] 1 = 1 :=
  iterate_fixed (map_one f) n

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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