ext

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule

URI: https://scilib.ai/kg/mathlib#HomogeneousSubmodule.ext

English

Two homogeneous submodules are equal if their underlying submodules are equal.

Русский

Два однородных подмодуля равны, если их базовые подмодули равны.

LaTeX

$$$$ \text{ext}: I.toSubmodule = J.toSubmodule \Rightarrow I = J. $$$$

Lean4

@[ext]
theorem ext {I J : HomogeneousSubmodule 𝒜 ℳ} (h : I.toSubmodule = J.toSubmodule) : I = J :=
  HomogeneousSubmodule.toSubmodule_injective _ _ h

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

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

Разделы

Аффилиация

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