restrict — Mathlib

English

Given a submodule p and a nilpotent endomorphism f, the induced quotient map on p is nilpotent as well.

Русский

При нильпотентном $f$ порожденный по $p$ отображение тождественно нильпотентно на $p$.

LaTeX

$$IsNilpotent (p.mapQ p f hp)$$

Lean4

theorem restrict {f : M →ₗ[R] M} {p : Submodule R M} (hf : MapsTo f p p) (hnil : IsNilpotent f) :
    IsNilpotent (f.restrict hf) := by
  obtain ⟨n, hn⟩ := hnil
  exact
    ⟨n,
      LinearMap.ext fun m ↦ by
        simp only [Module.End.pow_restrict n, hn, LinearMap.restrict_apply, LinearMap.zero_apply]; rfl⟩

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