mem_posSubgroup — Mathlib

English

An element u of Units R lies in the posSubgroup iff its underlying element is positive.

Русский

Элемент u из Units R принадлежит posSubgroup тогда, когда соответствующий элемент положителен.

LaTeX

$$$u \in \text{Units.posSubgroup } R \iff 0 < u$$$

Lean4

@[simp]
theorem mem_posSubgroup {R : Type*} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] (u : Rˣ) :
    u ∈ Units.posSubgroup R ↔ (0 : R) < u :=
  Iff.rfl

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