range_pow_padicValNat_subset_divisors'

English

The image of p^{t+1} for t in range(padicValNat p n) is contained in n.divisors without 1.

Русский

Образ p^{t+1} для t в диапазоне v_p(n) содержится в делителях n без 1.

LaTeX

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

Lean4

theorem range_pow_padicValNat_subset_divisors' {n : ℕ} [hp : Fact p.Prime] :
    ((Finset.range (padicValNat p n)).image fun t => p ^ (t + 1)) ⊆ n.divisors.erase 1 :=
  by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp
  intro t ht
  simp only [Finset.mem_image, Finset.mem_range] at ht
  obtain ⟨k, hk, rfl⟩ := ht
  rw [Finset.mem_erase, Nat.mem_divisors]
  refine ⟨?_, (pow_dvd_pow p <| succ_le_iff.2 hk).trans pow_padicValNat_dvd, hn⟩
  exact (Nat.one_lt_pow k.succ_ne_zero hp.out.one_lt).ne'

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