not_prime_pow — Mathlib

English

For not all exponents n, a^n is prime; specifically, if n ≠ 1, then a^n is not prime.

Русский

Не для каждого n элемент a^n является простым; особенно если n ≠ 1, то a^n не простое.

LaTeX

$$$\\forall n:\\, \\mathbb{N},\\; n \\neq 1 \\Rightarrow \\lnot \\operatorname{Prime}(a^n).$$$

Lean4

theorem not_prime_pow {n : ℕ} (hn : n ≠ 1) : ¬Prime (a ^ n) := fun hp => not_irreducible_pow hn hp.irreducible

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