baseChange_bot

Mathlib.LinearAlgebra.TensorProduct.Tower

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

English

Base-change of the bottom submodule is bottom: (⊥ : Submodule_R M).baseChange A = ⊥.

Русский

Расширение нуля подмодуля даёт ноль: (⊥ : Submodule_R M).baseChange A = ⊥.

LaTeX

$$$$ (\\perp) baseChange A = \\perp. $$$$

Lean4

@[simp]
theorem baseChange_bot : (⊥ : Submodule R M).baseChange A = ⊥ := by simp [baseChange_eq_span]

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

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

Разделы

Аффилиация

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