toSubalgebra_toSubmodule

Mathlib.Algebra.Algebra.Subalgebra.Basic

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

← MathLib Explorer

English

The submodule underlying a subalgebra is recovered by the same carrier.

Русский

Подмодуль, лежащий в основе подалгебры, восстанавливается тем же носителем.

LaTeX

$$$(S.toSubmodule.toSubalgebra S.one_mem f) = S$$$

Lean4

@[simp]
theorem toSubalgebra_toSubmodule (p : Submodule R A) (h_one h_mul) :
    Subalgebra.toSubmodule (p.toSubalgebra h_one h_mul) = p :=
  SetLike.coe_injective rfl

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

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

Разделы

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

Аффилиация

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