toNonUnitalSubring_inj

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

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

← MathLib Explorer

English

For S,U, S.toNonUnitalSubring = U.toNonUnitalSubring iff S = U.

Русский

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

LaTeX

$$$\forall S,U \; S.toNonUnitalSubring = U.toNonUnitalSubring \iff S = U$$$

Lean4

theorem toNonUnitalSubring_inj {S U : NonUnitalSubalgebra R A} : S.toNonUnitalSubring = U.toNonUnitalSubring ↔ S = U :=
  toNonUnitalSubring_injective.eq_iff

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

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

Разделы

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

Аффилиация

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