tmul_mem_baseChange_of_mem

Mathlib.LinearAlgebra.TensorProduct.Tower

URI: https://scilib.ai/kg/mathlib#Submodule.tmul_mem_baseChange_of_mem

English

If a ∈ A and m ∈ p with p a submodule of M, then a ⊗ m lies in p.baseChange A.

Русский

Если a ∈ A и m ∈ p, то a ⊗ m принадлежит p.baseChange A, где p ⊆ M.

LaTeX

$$$$ a\\otimes_R m \\in p.baseChange A,$$ при условии m ∈ p.$$

Lean4

theorem tmul_mem_baseChange_of_mem (a : A) {m : M} (hm : m ∈ p) : a ⊗ₜ[R] m ∈ p.baseChange A :=
  ⟨a ⊗ₜ[R] ⟨m, hm⟩, rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru