smul_iterate_apply

Mathlib.Algebra.Group.Action.Defs

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

English

Applying the n-th iterate to x equals a^n acting on x: (a • ·)^[n] x = a^n • x.

Русский

Применение n-й итерации к x равно a^n • x: (a • ·)^[n] x = a^n • x.

LaTeX

$$$\\\\forall a \\\\in M, \\\\forall n \\\\in \\mathbb{N}, \\\\forall x \\\\in α, \\\\ (a \\\\cdot ·)^[n] x = a^n \\\\cdot x.$$$

Lean4

@[to_additive]
theorem smul_iterate_apply (a : M) (n : ℕ) (x : α) : (a • ·)^[n] x = a ^ n • x := by rw [smul_iterate]

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

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

Разделы

Аффилиация

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