mk' — Mathlib

English

Construct a preordering from the same minimal axiom scheme for RingPreordering mk'.

Русский

Построить предпорядок по той же минимальной системе аксиом RingPreordering mk'.

LaTeX

$$Definition mk' as RingPreordering R with prescribed axioms$$

Lean4

/-- Construct a preordering from a minimal set of axioms. -/
def mk' {R : Type*} [CommRing R] (P : Set R) (add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P)
    (mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P) (sq : ∀ x : R, x * x ∈ P) (neg_one : -1 ∉ P) : RingPreordering R
    where
  carrier := P
  add_mem' {x y} := by simpa using add
  mul_mem' {x y} := by simpa using mul
  zero_mem' := by simpa using sq 0
  one_mem' := by simpa using sq 1

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