prime_of_irreducible_absNorm_span

English

If a ≠ 0 and hI asserts irreducible(absNorm(span {a})), then a is prime.

Русский

Если a ≠ 0 и hI утверждает ирредуцируемость(absNorm(span {a})), тогда a простое.

LaTeX

$$Prime(a) given a ≠ 0 and irreducible(absNorm(span {a})).$$

Lean4

theorem prime_of_irreducible_absNorm_span {a : S} (ha : a ≠ 0)
    (hI : Irreducible (Ideal.absNorm (Ideal.span ({ a } : Set S)))) : Prime a :=
  (Ideal.span_singleton_prime ha).mp (isPrime_of_irreducible_absNorm hI)

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