posSubmonoid — Mathlib

English

The submonoid of elements with positive valuation is the set {x | 0 <ᵥ x} with closure under multiplication and 1.

Русский

Подмоноид элементов с положительной оценкой — множество {x | 0 <ᵥ x}, замкнутое по умножению и содержащее единицу.

LaTeX

$$$\text{posSubmonoid } R = \{ x \in R \mid 0 <\!_v x \}$, with $\text{mul_mem'}$ and $\text{one_mem'}$ shown.$$

Lean4

/-- The submonoid of elements `x : R` whose valuation is positive. -/
def posSubmonoid : Submonoid R where
  carrier := {x | 0 <ᵥ x}
  mul_mem' := zero_srel_mul
  one_mem' := zero_srel_one

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