not_isPrime_iff — Mathlib

English

¬IsPrime(I) iff I = ⊤ or there exist x ∉ I and y ∉ I with x y ∈ I.

Русский

¬IsPrime(I) эквивалентно I = ⊤ или существуют x ∉ I и y ∉ I такие, что x y ∈ I.

LaTeX

$$¬\text{IsPrime}(I) \iff I = \top \lor \exists x (x \notin I) \land \exists y (y \notin I) \land x y \in I$$

Lean4

theorem not_isPrime_iff {I : Ideal α} : ¬I.IsPrime ↔ I = ⊤ ∨ ∃ (x : α) (_hx : x ∉ I) (y : α) (_hy : y ∉ I), x * y ∈ I :=
  by
  simp_rw [Ideal.isPrime_iff, not_and_or, Ne, Classical.not_not, not_forall, not_or]
  exact
    or_congr Iff.rfl ⟨fun ⟨x, y, hxy, hx, hy⟩ => ⟨x, hx, y, hy, hxy⟩, fun ⟨x, hx, y, hy, hxy⟩ => ⟨x, y, hxy, hx, hy⟩⟩

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