instMonoidSubtypeLtOfNat — Mathlib

English

Let R be a strict ordered ring. Then the positive subset { x ∈ R | 0 < x } forms a Monoid under multiplication with identity 1.

Русский

Пусть R — строго упорядоченное кольцо. Тогда положительная часть образует моноид под умножением с единицей 1.

LaTeX

$$$\\\\forall a,b \\\\in \\\\{ x : R \\\\mid 0 < x \\\\}, (a \\\\cdot b) \\\\in \\\\{ x : R \\\\mid 0 < x \\\\}$ and $1 \\\\cdot a = a$ and $a \\\\cdot 1 = a.$$$

Lean4

instance : Monoid { x : R // 0 < x } :=
  fast_instance%Subtype.coe_injective.monoid _ val_one val_mul val_pow

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