mk' — Mathlib

English

Given a RingPreordering P on a commutative ring R and a hypothesis that if x*y ∈ P.support then x ∈ P.support or y ∈ P.support, then P becomes an IsOrdering.

Русский

Пусть P — RingPreordering на кольце R и дано условие, что если x·y ∈ P.support, то x ∈ P.support или y ∈ P.support; тогда P образует IsOrdering.

LaTeX

$$P.IsOrdering$$

Lean4

/-- Constructor for IsOrdering that doesn't require `ne_top'`. -/
theorem mk' [HasMemOrNegMem P] (h : ∀ {x y}, x * y ∈ P.support → x ∈ P.support ∨ y ∈ P.support) : P.IsOrdering
    where
  ne_top' := support_ne_top P
  mem_or_mem' := h

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