instHasIdealSupportOfHasMemOrNegMem

English

If HasMemOrNegMem holds for a RingPreordering P, then P has HasIdealSupport, i.e., the ideal-support structure can be constructed using the mem-or-neg-mem property.

Русский

Если для RingPreordering P выполняется свойство HasMemOrNegMem, то P имеет HasIdealSupport, то есть опорная идеальная структура строится с использованием свойства mem-or-neg-mem.

LaTeX

$$$[HasMemOrNegMem\\, P] \\Rightarrow P.HasIdealSupport$$$

Lean4

instance [HasMemOrNegMem P] : P.HasIdealSupport where
  smul_mem_support x a
    ha :=
    match mem_or_neg_mem P x with
    | .inl hx => ⟨by simpa using mul_mem hx ha.1, by simpa using mul_mem hx ha.2⟩
    | .inr hx => ⟨by simpa using mul_mem hx ha.2, by simpa using mul_mem hx ha.1⟩

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