tmul_mem_baseChange_of_mem — Mathlib

English

Let N be a LieSubmodule of a Lie module M over R, and let A be an R-algebra. For any a in A and any m in N, the tensor a ⊗ m lies in the base change of N to A.

Русский

Пусть N — подмодуль Ли в модуле M над R, A — алгебра над R. Тогда для любого a ∈ A и любого m ∈ N имеет место a ⊗ m ∈ базисное изменение N над A.

LaTeX

$$$ a \\otimes_R m \\in \\operatorname{baseChange}_A(N) $$$

Lean4

theorem tmul_mem_baseChange_of_mem (a : A) {m : M} (hm : m ∈ N) : a ⊗ₜ[R] m ∈ N.baseChange A :=
  (N : Submodule R M).tmul_mem_baseChange_of_mem a hm

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