instMulSubtypeLtOfNat_mathlib — Mathlib

English

Let R be a strict ordered ring and 0 < x for x in the positive subtype of R. Then multiplication on { x ∈ R | 0 < x } is well-defined: if x,y > 0 then x · y > 0.

Русский

Пусть R — строго упорядченное кольцо. Тогда умножение на { x ∈ R | 0 < x } определено так, что если x > 0 и y > 0, то x·y > 0.

LaTeX

$$$\\\\forall x,y \\\\in \\\\{ x : R \\\\mid 0 < x \\\\}, 0 < x \\\\cdot y.$$$

Lean4

instance : Mul { x : R // 0 < x } :=
  ⟨fun x y => ⟨x * y, mul_pos x.2 y.2⟩⟩

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