ext

Mathlib.Algebra.Ring.Subring.Defs

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

← MathLib Explorer

English

Two subrings are equal if they have the same elements.

Русский

Два подкольца равны тогда и только тогда, когда у них совпадают элементы.

LaTeX

$$$ S = T \\iff \\forall x, x \\in S \\leftrightarrow x \\in T $$$

Lean4

/-- Two subrings are equal if they have the same elements. -/
@[ext]
theorem ext {S T : Subring R} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T :=
  SetLike.ext h

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

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

Разделы

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

Аффилиация

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