English
If α and β are ordered rings (with the appropriate algebraic structures), then their product ring α × β is also an ordered ring.
Русский
Если α и β являются упорядоченными кольцами, то произведение α × β также является упорядоченным кольцом.
LaTeX
$$IsOrderedRing(α × β)$$
Lean4
instance [Semiring α] [PartialOrder α] [IsOrderedRing α] [Semiring β] [PartialOrder β] [IsOrderedRing β] :
IsOrderedRing (α × β) :=
{ zero_le_one := ⟨zero_le_one, zero_le_one⟩
mul_le_mul_of_nonneg_left := fun _ _ _ hab hc =>
⟨mul_le_mul_of_nonneg_left hab.1 hc.1, mul_le_mul_of_nonneg_left hab.2 hc.2⟩
mul_le_mul_of_nonneg_right := fun _ _ _ hab hc =>
⟨mul_le_mul_of_nonneg_right hab.1 hc.1, mul_le_mul_of_nonneg_right hab.2 hc.2⟩ }
