mem_mk' — Mathlib

English

Let R be a commutative ring and P a RingPreordering on R. Then for every element x in R, x belongs to mk'(P) if and only if x belongs to P.

Русский

Пусть R — коммутативное кольцо, P — RingPreordering на R. Тогда для любого x ∈ R выполняется x ∈ mk'(P) тогда и только тогда, когда x ∈ P.

LaTeX

$$$\forall x\, x \in \mathrm{mk}'(P) \iff x \in P$$$

Lean4

@[simp]
theorem mem_mk' {x : R} : x ∈ mk' P add mul sq neg_one ↔ x ∈ P :=
  .rfl

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