exists_eq_pow_mul_and_not_dvd — Mathlib

English

For any nonzero n and any p ≠ 1, there exist e and n' with p ∤ n' and n = p^e n'.

Русский

Для любого ненулевого n и любого p ≠ 1 существуют e и n' такие, что p не делит n' и n = p^e n'.

LaTeX

$$$$ \exists e,n'\in\mathbb{N},\ p \neq 1:\ p \nmid n' \land n = p^{e} \cdot n'. $$$$

Lean4

/-- If `n` is a nonzero natural number and `p ≠ 1`, then there are natural numbers `e`
and `n'` such that `n'` is not divisible by `p` and `n = p^e * n'`. -/
theorem exists_eq_pow_mul_and_not_dvd {n : ℕ} (hn : n ≠ 0) (p : ℕ) (hp : p ≠ 1) :
    ∃ e n' : ℕ, ¬p ∣ n' ∧ n = p ^ e * n' :=
  let ⟨a', h₁, h₂⟩ := (Nat.finiteMultiplicity_iff.mpr ⟨hp, Nat.pos_of_ne_zero hn⟩).exists_eq_pow_mul_and_not_dvd
  ⟨_, a', h₂, h₁⟩

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