toSubmodule_injective

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalSubalgebra.toSubmodule_injective

← MathLib Explorer

English

The map toSubmodule : NonUnitalSubalgebra(R,A) → Submodule(R,A) is injective.

Русский

Отображение toSubmodule: NonUnitalSubalgebra(R,A) → Submodule(R,A) инъективно.

LaTeX

$$$\text{Injective}(\text{toSubmodule})$$$

Lean4

theorem toSubmodule_injective : Function.Injective (toSubmodule : NonUnitalSubalgebra R A → Submodule R A) :=
  fun S T h => ext fun x => by rw [← mem_toSubmodule, ← mem_toSubmodule, h]

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

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

Разделы

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

Аффилиация

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