smul — Mathlib

English

If a ∈ S is nilpotent and R acts on S with zero compatibility, then t·a is nilpotent for any t ∈ R.

Русский

Пусть a ∈ S нильпотентно; если R действует на S с нулевой совместимостью, то для любого t ∈ R произведение t·a нильпотентно.

LaTeX

$$$ \\text{IsNilpotent}(a) \\Rightarrow \\text{IsNilpotent}(t \\cdot a) \\quad(\\text{for all } t \\in R)$$$

Lean4

theorem smul [MonoidWithZero R] [MonoidWithZero S] [MulActionWithZero R S] [SMulCommClass R S S] [IsScalarTower R S S]
    {a : S} (ha : IsNilpotent a) (t : R) : IsNilpotent (t • a) :=
  by
  obtain ⟨k, ha⟩ := ha
  use k
  rw [smul_pow, ha, smul_zero]

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