English
P is an IsOrdering if and only if for all a, b in R, whenever -(a*b) ∈ P, then a ∈ P or b ∈ P.
Русский
P является IsOrdering тогда, когда для всех a, b ∈ R, если -(a b) ∈ P, то a ∈ P или b ∈ P.
LaTeX
$$P.IsOrdering \iff (\forall a, b \in R, -(a b) \in P \rightarrow a \in P \lor b \in P)$$
Lean4
theorem isOrdering_iff : P.IsOrdering ↔ ∀ a b : R, -(a * b) ∈ P → a ∈ P ∨ b ∈ P :=
by
refine ⟨fun _ a b _ => ?_, fun h => ?_⟩
· by_contra
have : a * b ∈ P := by simpa using mul_mem (by aesop : -a ∈ P) (by aesop : -b ∈ P)
have : a ∈ P.support ∨ b ∈ P.support := Ideal.IsPrime.mem_or_mem inferInstance (by simp_all [mem_support])
simp_all [mem_support]
· have : HasMemOrNegMem P := ⟨by simp [h]⟩
refine IsOrdering.mk' P (fun {x y} _ => ?_)
by_contra
have := h (-x) y
have := h (-x) (-y)
have := h x y
have := h x (-y)
cases (by aesop : x ∈ P ∨ -x ∈ P) <;> simp_all [mem_support]
