mapsTo_pow_toEnd_sub_algebraMap — Mathlib

English

The k-th power of the operator (toEnd x − algebraMap φ) maps the LieSubmodule N into itself, for any φ ∈ R and x ∈ L.

Русский

Степень k оператора (toEnd x − algebraMap φ) отображает N в себя для любого φ ∈ R и x ∈ L.

LaTeX

$$$\text{MapsTo}((\mathrm{toEnd}_{R,L,M} x - \mathrm{algebraMap}_R(\mathrm{Module.End}_R M) \varphi)^k, N, N)$$$

Lean4

theorem mapsTo_pow_toEnd_sub_algebraMap {φ : R} {k : ℕ} {x : L} :
    MapsTo ((toEnd R L M x - algebraMap R (Module.End R M) φ) ^ k) N N :=
  by
  rw [Module.End.coe_pow]
  exact MapsTo.iterate (fun m hm ↦ N.sub_mem (N.lie_mem hm) (N.smul_mem _ hm)) k

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