isPrime — Mathlib

English

In a Boolean algebra, a maximal ideal is prime.

Русский

В булевой алгебре максимальный идеал является простым.

LaTeX

$$$\\text{IsMaximal}(I) \\Rightarrow IsPrime I$$$

Lean4

instance (priority := 100) isPrime [IsMaximal I] : IsPrime I :=
  by
  rw [isPrime_iff_mem_or_mem]
  intro x y
  contrapose!
  rintro ⟨hx, hynI⟩ hxy
  apply hynI
  let J := I ⊔ principal x
  have hJuniv : (J : Set P) = Set.univ := IsMaximal.maximal_proper (lt_sup_principal_of_notMem ‹_›)
  have hyJ : y ∈ (J : Set P) := Set.eq_univ_iff_forall.mp hJuniv y
  rw [coe_sup_eq] at hyJ
  rcases hyJ with ⟨a, ha, b, hb, hy⟩
  rw [hy]
  refine sup_mem ha (I.lower (le_inf hb ?_) hxy)
  rw [hy]
  exact le_sup_right

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