lie_f_pow_toEnd_f

Mathlib.Algebra.Lie.Sl2

URI: https://scilib.ai/kg/mathlib#IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f

English

For a primitive vector P, the Lie action of f on ψ_n advances the index by one: [f, ψ_n] = ψ_{n+1}.

Русский

Для примитивного вектора P действие f на ψ_n увеличивает индекс на единицу: [f, ψ_n] = ψ_{n+1}.

LaTeX

$$[f, ψ_n] = ψ_{n+1}$$

Lean4

@[nolint unusedArguments]
theorem lie_f_pow_toEnd_f (P : HasPrimitiveVectorWith t m μ) (n : ℕ) : ⁅f, ψ n⁆ = ψ(n + 1) := by simp [pow_succ']

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

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

Разделы

Аффилиация

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