isPrimePow_iff_pow_succ
theorem isPrimePow_iff_pow_succ :
∀ {R : Type u_1} [inst : CommMonoidWithZero R] (n : R), IsPrimePow n ↔ ∃ p k, Prime p ∧ p ^ (k + 1) = n
The theorem `isPrimePow_iff_pow_succ` provides an equivalent definition for prime powers in the context of a commutative monoid with zero (such as a ring). It states that an element `n` is a prime power if and only if there exists a prime number `p` and a natural number `k` such that `n` can be expressed as `p` to the power of `(k+1)`. Here, a prime number `p` is an element that is not zero, not a unit, and if `p` divides the product of `a` and `b`, then `p` must divide `a` or `b`.
More concisely: An element is a prime power in a commutative monoid with zero if and only if it can be expressed as the power of some prime element plus one.
|
isPrimePow_nat_iff
theorem isPrimePow_nat_iff : ∀ (n : ℕ), IsPrimePow n ↔ ∃ p k, p.Prime ∧ 0 < k ∧ p ^ k = n
The theorem `isPrimePow_nat_iff` states that for every natural number `n`, `n` is a prime power if and only if there exist a natural number `p` and `k` such that `p` is a prime number, `k` is greater than 0, and `n` is equal to `p` raised to the power `k`. In mathematical terms, it expresses the equivalence of the two conditions "n is a prime power" and "there exist p and k such that p is a prime number, k is a positive number, and n equals p to the power of k".
More concisely: A natural number `n` is a prime power if and only if there exists a prime number `p` and a positive integer `k` such that `n = p^k`.
|
not_isPrimePow_zero
theorem not_isPrimePow_zero :
∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : NoZeroDivisors R], ¬IsPrimePow 0
The theorem `not_isPrimePow_zero` states that, for all types `R` which have an instance of `CommMonoidWithZero` and `NoZeroDivisors`, zero is not a prime power. In other words, there does not exist a prime number `p` and a positive natural number `k` such that `p` raised to the power of `k` equals zero.
More concisely: For types endowed with a CommMonoidWithZero and NoZeroDivisors structure, zero has no prime power representation.
|