prime_span_singleton_iff — Mathlib

English

For any element a, Prime(span{a}) holds iff Prime(a) holds in the ring.

Русский

Для элемента a верно: Prime(span{a}) эквивалентно Prime(a) в кольце.

LaTeX

$$$\text{Prime}(\mathrm{Ideal}.\mathrm{span}\{a\}) \iff \text{Prime}(a)$$$

Lean4

@[simp]
theorem prime_span_singleton_iff {a : A} : Prime (Ideal.span { a }) ↔ Prime a :=
  by
  rcases eq_or_ne a 0 with rfl | ha
  · rw [Set.singleton_zero, span_zero, ← Ideal.zero_eq_bot, ← not_iff_not]
    simp only [not_prime_zero, not_false_eq_true]
  · have ha' : span { a } ≠ ⊥ := by simpa only [ne_eq, span_singleton_eq_bot] using ha
    rw [Ideal.prime_iff_isPrime ha', Ideal.span_singleton_prime ha]

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