primeCompl — Mathlib

English

The complement of a prime ideal P is a submonoid of the ambient ring; it contains 1 and is closed under multiplication.

Русский

Комплемент простого идеала P образует подмономоид кольца; он содержит 1 и замкнут по умножению.

LaTeX

$$P^{\mathrm{c}} \text{ is a submonoid of } \alpha, \ 1 \in P^{\mathrm{c}}, \ \forall x,y \in P^{\mathrm{c}},\ xy \in P^{\mathrm{c}}$$

Lean4

/-- The complement of a prime ideal `P ⊆ R` is a submonoid of `R`. -/
def primeCompl (P : Ideal α) [hp : P.IsPrime] : Submonoid α
    where
  carrier := (Pᶜ : Set α)
  one_mem' := P.one_notMem
  mul_mem' {_ _} hnx hny hxy := Or.casesOn (hp.mem_or_mem hxy) hnx hny

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