pow_minFac — Mathlib

English

For all n,k ∈ ℕ with k ≠ 0, minFac(n^k) = minFac(n).

Русский

Для всех n,k ∈ ℕ с k ≠ 0 следует minFac(n^k) = minFac(n).

LaTeX

$$$k \neq 0 \Rightarrow \minFac(n^k) = \minFac(n)$$$

Lean4

theorem pow_minFac {n k : ℕ} (hk : k ≠ 0) : (n ^ k).minFac = n.minFac :=
  by
  rcases eq_or_ne n 1 with (rfl | hn)
  · simp
  have hnk : n ^ k ≠ 1 := fun hk' => hn ((pow_eq_one_iff hk).1 hk')
  apply (minFac_le_of_dvd (minFac_prime hn).two_le ((minFac_dvd n).pow hk)).antisymm
  apply minFac_le_of_dvd (minFac_prime hnk).two_le ((minFac_prime hnk).dvd_of_dvd_pow (minFac_dvd _))

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