English
If an ideal is maximal with respect to not satisfying an Oka predicate, then it is prime.
Русский
Если идеал является максимальным по отношению к неисполнению предиката Ока, то он являетсяprime.
LaTeX
$$IsOka 최대 prime$$
Lean4
/-- If an ideal is maximal for not satisfying an Oka predicate then it is prime. -/
@[stacks 05KE]
theorem isPrime_of_maximal_not {I : Ideal R} (hI : Maximal (¬P ·) I) : I.IsPrime
where
ne_top' hI' := hI.prop (hI' ▸ hP.top)
mem_or_mem' := by
by_contra!
obtain ⟨a, b, hab, ha, hb⟩ := this
have h₁ : P (I ⊔ span { a }) := of_not_not <| hI.not_prop_of_gt (Submodule.lt_sup_iff_notMem.2 ha)
have h₂ : P (I.colon (span { a })) :=
of_not_not <|
hI.not_prop_of_gt <| lt_of_le_of_ne le_colon (fun H ↦ hb <| H ▸ mem_colon_singleton.2 (mul_comm a b ▸ hab))
exact hI.prop (hP.oka h₁ h₂)
