mul_mem_iff_mem_or_mem — Mathlib

English

If I is prime, then r^n ∈ I iff r ∈ I for n > 0.

Русский

Если I прост, то r^n ∈ I эквивалентно r ∈ I при n > 0.

LaTeX

$$I.IsPrime \Rightarrow ∀ (r) (n) (hn : 0 < n), r^{n} \in I \iff r \in I$$

Lean4

theorem mul_mem_iff_mem_or_mem {I : Ideal α} [I.IsTwoSided] (hI : I.IsPrime) : ∀ {x y : α}, x * y ∈ I ↔ x ∈ I ∨ y ∈ I :=
  @fun x y =>
    ⟨hI.mem_or_mem, by
      rintro (h | h)
      exacts [I.mul_mem_right y h, I.mul_mem_left x h]⟩

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