primeFactors_pow' — Mathlib

English

Let M be as above. For any a ∈ M and any n ∈ ℕ with n ≠ 0, the prime factors of a^n equal the prime factors of a.

Русский

Пусть M удовлетворяет условиям выше. Для любого a ∈ M и любого n ∈ ℕ, не равного нулю, простые делители a^n совпадают с простыми делителями a.

LaTeX

$$$ n \neq 0 \Rightarrow \operatorname{primeFactors}(a^n) = \operatorname{primeFactors}(a) $$$

Lean4

@[simp]
theorem primeFactors_pow' (a : M) {n : ℕ} [NeZero n] : primeFactors (a ^ n) = primeFactors a :=
  primeFactors_pow a NeZero.out

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