op_le_op_iff

Mathlib.Algebra.Ring.Subring.MulOpposite

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

English

Let S1,S2 be subrings of R. Then S1^{op} ⊆ S2^{op} if and only if S1 ⊆ S2.

Русский

Пусть S1,S2 — подкольца R. Тогда S1^{op} ⊆ S2^{op} эквивалентно S1 ⊆ S2.

LaTeX

$$$S_1^{op} \le S_2^{op} \iff S_1 \le S_2$$$

Lean4

@[simp]
theorem op_le_op_iff {S₁ S₂ : Subring R} : S₁.op ≤ S₂.op ↔ S₁ ≤ S₂ :=
  MulOpposite.op_surjective.forall

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

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

Разделы

Аффилиация

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