toSubsemiring_injective

Mathlib.Algebra.Order.Ring.Ordering.Defs

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

English

The mapping P ↦ P.toSubsemiring is injective: if P1.toSubsemiring = P2.toSubsemiring then P1 = P2.

Русский

Отображение P ↦ P.toSubsemiring инъективно: если P1.toSubsemiring = P2.toSubsemiring, тогда P1 = P2.

LaTeX

$$P_1.toSubsemiring = P_2.toSubsemiring \Rightarrow P_1 = P_2$$

Lean4

theorem toSubsemiring_injective : Function.Injective (toSubsemiring : RingPreordering R → _) := fun A B h => by ext;
  rw [h]

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

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

Разделы

Аффилиация

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