mul_le — Mathlib

English

If P is a prime ideal, then I·J ≤ P if and only if I ≤ P or J ≤ P.

Русский

Если P — простый идеал, то I·J ≤ P эквивалентно I ≤ P или J ≤ P.

LaTeX

$$$ P \text{prime} \Rightarrow (I \cdot J \le P) \iff (I \le P) \lor (J \le P) $$$

Lean4

theorem mul_le {I J P : Ideal R} (hp : IsPrime P) : I * J ≤ P ↔ I ≤ P ∨ J ≤ P :=
  by
  rw [or_comm, Ideal.mul_le]
  simp_rw [hp.mul_mem_iff_mem_or_mem, SetLike.le_def, ← forall_or_left, or_comm, forall_or_left]

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