toSubsemiring_inj

Mathlib.Algebra.Order.Ring.Ordering.Defs

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

English

The equality P1.toSubsemiring = P2.toSubsemiring is equivalent to P1 = P2.

Русский

Равенство P1.toSubsemiring = P2.toSubsemiring эквивалентно P1 = P2.

LaTeX

$$P_1.toSubsemiring = P_2.toSubsemiring \iff P_1 = P_2$$

Lean4

@[simp]
theorem toSubsemiring_inj {P₁ P₂ : RingPreordering R} : P₁.toSubsemiring = P₂.toSubsemiring ↔ P₁ = P₂ :=
  toSubsemiring_injective.eq_iff

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

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

Разделы

Аффилиация

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