coprime_of_ne — Mathlib

English

Two distinct maximal ideals are comaximal: their sum is the whole ring, i.e., M + M' = ⊤.

Русский

Два различных максимальных идеала совместно порождают всю кольцо: сумма M + M' равна ⊤.

LaTeX

$$$M \neq M' \implies M \!+\! M' = \top$$$

Lean4

theorem coprime_of_ne {M M' : Ideal α} (hM : M.IsMaximal) (hM' : M'.IsMaximal) (hne : M ≠ M') : M ⊔ M' = ⊤ :=
  by
  contrapose! hne with h
  exact hM.eq_of_le hM'.ne_top (le_sup_left.trans_eq (hM'.eq_of_le h le_sup_right).symm)

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