toEnd_pow_comp_lieHom — Mathlib

English

Applying a Lie module homomorphism f after raising to a power k commutes with applying the endomorphism power on the domain, i.e., toEnd^k f = f ∘ toEnd^k.

Русский

Применение гомоморфизма Ли f после возведения в степень k коммутирует с применением соответствующего конца: toEnd^k f = f ∘ toEnd^k.

LaTeX

$$$ (\,toEnd_{R,L,M} x^k\, ) \circ f = f \circ (\,toEnd_{R,L,M} x^k\,)$$$

Lean4

theorem toEnd_pow_comp_lieHom : (toEnd R L M₂ x ^ k) ∘ₗ f = f ∘ₗ toEnd R L M x ^ k :=
  by
  apply Module.End.commute_pow_left_of_commute
  ext
  simp

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