prime_generator_of_isPrime — Mathlib

English

For a principal span of s, r divides the generator of span s iff r divides every x in s.

Русский

Для главного окна порождения span s, r делит генератор span s тогда и только тогда, когда r делит каждый элемент x ∈ s.

LaTeX

$$r ∣ generator (Ideal.span s) ↔ ∀ x ∈ s, r ∣ x$$

Lean4

theorem prime_generator_of_isPrime (S : Ideal R) [S.IsPrincipal] [is_prime : S.IsPrime] (ne_bot : S ≠ ⊥) :
    Prime (generator S) :=
  ⟨fun h => ne_bot ((eq_bot_iff_generator_eq_zero S).2 h), fun h =>
    is_prime.ne_top (S.eq_top_of_isUnit_mem (generator_mem S) h), fun _ _ => by
    simpa only [← mem_iff_generator_dvd S] using is_prime.2⟩
    -- Note that the converse may not hold if `ϕ` is not injective.

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