toSubmodule_inj

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

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

English

For S,U as NonUnitalSubalgebras, S.toSubmodule = U.toSubmodule if and only if S = U.

Русский

Для таких S,U: S.toSubmodule = U.toSubmodule тогда и только тогда, когда S = U.

LaTeX

$$$\forall S,U : \text{NonUnitalSubalgebra}(R,A),\; S.toSubmodule = U.toSubmodule \iff S = U$$$

Lean4

theorem toSubmodule_inj {S U : NonUnitalSubalgebra R A} : S.toSubmodule = U.toSubmodule ↔ S = U :=
  toSubmodule_injective.eq_iff

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

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

Разделы

Аффилиация

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