coe_toEnd_pow — Mathlib

English

For a Lie submodule N ⊆ M, the n-th power of the endomorphism x acting on N coincides with its n-th power on M when evaluated on N.

Русский

Для подмодуля N ⊆ M n-я степень-endomorphism x действует на N так же, как и на M, при вычислении на элементах N.

LaTeX

$$$\forall n\in\mathbb{N},\; ((\mathrm{toEnd}_{R,L,N}(x))^n)(y) = ((\mathrm{toEnd}_{R,L,M}(x))^n)(y)$ для всех $y\in N$$$

Lean4

theorem coe_toEnd_pow (N : LieSubmodule R L M) (x : L) (y : N) (n : ℕ) :
    ((toEnd R L N x ^ n) y : M) = (toEnd R L M x ^ n) y := by
  induction n generalizing y with
  | zero => rfl
  | succ n ih => simp only [pow_succ', Module.End.mul_apply, ih, LieSubmodule.coe_toEnd]

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