English
If I is a maximal ideal, then I is a prime ideal.
Русский
Если I максимальный идеал, то I является простым идеал.
LaTeX
$$$I\text{ maximal} \Rightarrow I\text{ prime}$$$
Lean4
theorem isPrime {I : Ideal α} (H : I.IsMaximal) : I.IsPrime :=
⟨H.1.1,
@fun x y hxy =>
or_iff_not_imp_left.2 fun hx => by
let J : Ideal α := Submodule.span α (insert x ↑I)
have IJ : I ≤ J := Set.Subset.trans (subset_insert _ _) subset_span
have xJ : x ∈ J := Ideal.subset_span (Set.mem_insert x I)
obtain ⟨_, oJ⟩ := isMaximal_iff.1 H
specialize oJ J x IJ hx xJ
rcases Submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩
obtain F : y * 1 = y * (a • x + b) := congr_arg (fun g : α => y * g) oe
rw [← mul_one y, F, mul_add, mul_comm, smul_eq_mul, mul_assoc]
refine Submodule.add_mem I (I.mul_mem_left a hxy) (Submodule.smul_mem I y ?_)
rwa [Submodule.span_eq] at h⟩
-- see Note [lower instance priority]
