toSubMulAction_injective

Mathlib.Algebra.Module.Submodule.Defs

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

← MathLib Explorer

English

The map from Submodule to SubMulAction is injective.

Русский

Отображение подмодуля в SubMulAction инъективно.

LaTeX

$$toSubMulAction: Submodule R M → SubMulAction R M is injective$$

Lean4

theorem toSubMulAction_injective : Injective (toSubMulAction : Submodule R M → SubMulAction R M) := fun p q h =>
  SetLike.ext'_iff.2 (show (p.toSubMulAction : Set M) = q from SetLike.ext'_iff.1 h)

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

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

Разделы

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

Аффилиация

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