span_singleton_prime — Mathlib

English

For a commutative semiring α and p ≠ 0, the ideal generated by p is prime iff p is a prime element.

Русский

Для коммутативного полукольца α и p ≠ 0, идеал, порожденный p, прост тогда и только тогда, когда p — простое элемент.

LaTeX

$$$p \neq 0 \Rightarrow \text{span}({p}) \text{ isPrime} \iff \text{Prime}(p)$$

Lean4

theorem span_singleton_prime {p : α} (hp : p ≠ 0) : IsPrime (span ({ p } : Set α)) ↔ Prime p := by
  simp [isPrime_iff, Prime, span_singleton_eq_top, hp, mem_span_singleton]

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