## Stream: Is there code for X?

### Topic: Maximal ideals are pairwise coprime

#### Thomas Browning (Jan 03 2021 at 19:19):

Does mathlib know that maximal ideals (ideal.is_maximal) are pairwise coprime? Context: I want to apply the Chinese Remainder Theorem (ideal.quotient_inf_ring_equiv_pi_quotient) to some maximal ideals. It would follow from this generalized lemma about coatoms:

lemma lem1 {α : Type*} [complete_lattice α] {a b : α} (ha : is_coatom a) (hb : is_coatom b) (h : a ≠ b) : a ⊔ b = ⊤ :=
begin
have h1 := eq_top_or_eq_of_coatom_le ha le_sup_left,
cases h1,
{ exact h1 },
have h2 := eq_top_or_eq_of_coatom_le hb le_sup_right,
cases h2,
{ exact h2 },
exact false.rec _ (h (le_antisymm (sup_eq_right.mp h2) (sup_eq_left.mp h1))),
end


#### Aaron Anderson (Jan 03 2021 at 19:25):

I don't know the answer yet to whether we have the right version for the CRT, but I do know that the coatom lemma should totally be PR'd. I just added atoms and coatoms, so the API's not all there

#### Aaron Anderson (Jan 03 2021 at 19:28):

I could write that PR if you'd like, but if you do it, I think it only needs [semilattice_sup_top], and there should also be a version for is_atom.

#### Thomas Browning (Jan 03 2021 at 19:32):

Sure, I can do it

#### Thomas Browning (Jan 03 2021 at 20:03):

#5596

Last updated: May 16 2021 at 05:21 UTC