properDivisors_prime_pow — Mathlib

English

For a prime p and natural k, the proper divisors of p^k are exactly the powers p^j with 0 ≤ j < k.

Русский

Для простого p и натурального k правильные делители p^k равны точно степеням p^j при 0 ≤ j < k.

LaTeX

$$$\operatorname{properDivisors}(p^k) = \{ p^j : 0 \le j < k \}. $$$

Lean4

theorem properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) :
    properDivisors (p ^ k) = (Finset.range k).map ⟨(p ^ ·), Nat.pow_right_injective pp.two_le⟩ :=
  by
  ext a
  simp only [mem_properDivisors, mem_map, mem_range, Function.Embedding.coeFn_mk]
  have := mem_properDivisors_prime_pow pp k (x := a)
  rw [mem_properDivisors] at this
  grind

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