range_mapIncl

Mathlib.LinearAlgebra.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#TensorProduct.range_mapIncl

← MathLib Explorer

English

Range equals the span of all f(m) ⊗ g(n).

Русский

Образ равен спану всех элементов f(m) ⊗ g(n).

LaTeX

$$$\\operatorname{range}(\\mathrm{map}\\ f\\ g) = \\operatorname{span}_R\\{ f(m) \\otimes_R g(n) \\mid m,n \\}$$$

Lean4

theorem range_mapIncl (p : Submodule R P) (q : Submodule R Q) : LinearMap.range (mapIncl p q) = .map₂ (mk R _ _) p q :=
  by simp_rw [mapIncl, range_map, Submodule.range_subtype]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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