coe_ad_pow — Mathlib

English

The n-th iterate of the adjoint action on a Lie subalgebra H agrees with the n-th iterate on L, restricted to H.

Русский

N-ая итерация ад-оператора на подалгебре H совпадает с N-й итерацией на L, ограниченной до H.

LaTeX

$$$\forall H\subseteq L,\; \big((\mathrm{ad}_H x)^n(y)\big) = \big((\mathrm{ad}_L x)^n(y)\big)$ for all $x,y\in H$, $n\in\mathbb{N}$$$

Lean4

theorem coe_ad_pow (H : LieSubalgebra R L) (x y : H) (n : ℕ) : ((ad R H x ^ n) y : L) = (ad R L x ^ n) y :=
  LieSubmodule.coe_toEnd_pow R H L H.toLieSubmodule x y n

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