toSubsemiring_inj

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Subalgebra.toSubsemiring_inj

English

Two subalgebras are equal iff their underlying subsemirings are equal.

Русский

Две подалгебры равны тогда и только тогда, когда равны их базовые подсемиринги.

LaTeX

$$$ S^{\mathrm{toSubsemiring}} = U^{\mathrm{toSubsemiring}} \iff S = U $$$

Lean4

theorem toSubsemiring_inj {S U : Subalgebra R A} : S.toSubsemiring = U.toSubsemiring ↔ S = U :=
  toSubsemiring_injective.eq_iff

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

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

Разделы

Аффилиация

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