instIsNilpotentTensor — Mathlib

English

If L is nilpotent on M, then the tensor extension A⊗R L is nilpotent on A⊗R M.

Русский

Если L нильпотентен на M, то тензорное расширение A⊗R L нильпотентно на A⊗R M.

LaTeX

$$[IsNilpotent L M] ⇒ IsNilpotent (TensorProduct R A L) (TensorProduct R A M)$$

Lean4

instance instIsNilpotentTensor [IsNilpotent L M] : IsNilpotent (A ⊗[R] L) (A ⊗[R] M) :=
  by
  obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L M
  rw [isNilpotent_iff A]
  exact ⟨k, by simp [hk]⟩

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