range_pow_padicValNat_subset_divisors

English

The powers p^k with k up to padicValNat p n are divisors of n, for n ≠ 0.

Русский

Степени p^k с k до v_p(n) являются делителями n для n ≠ 0.

LaTeX

$$$\\forall p,n\\in\\mathbb{N},\\ n \\neq 0 \\Rightarrow (\\operatorname{range}(\\operatorname{padicValNat} p n + 1)).image(p^\\cdot) \\subseteq n.divisors$$$

Lean4

theorem range_pow_padicValNat_subset_divisors {n : ℕ} (hn : n ≠ 0) :
    (Finset.range (padicValNat p n + 1)).image (p ^ ·) ⊆ n.divisors :=
  by
  intro t ht
  simp only [Finset.mem_image, Finset.mem_range] at ht
  obtain ⟨k, hk, rfl⟩ := ht
  rw [Nat.mem_divisors]
  exact ⟨(pow_dvd_pow p <| by cutsat).trans pow_padicValNat_dvd, hn⟩

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