mem_divisors_prime_pow — Mathlib

English

Let p be prime. The divisors of p^k are exactly p^j for j = 0,1,...,k.

Русский

Пусть p — простое число. Делители p^k состоят ровно из p^j для j = 0,1,...,k.

LaTeX

$$$ x \in \mathrm{divisors}(p^k) \iff \exists j \le k,\ x = p^j $$$

Lean4

theorem mem_divisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} : x ∈ divisors (p ^ k) ↔ ∃ j ≤ k, x = p ^ j := by
  rw [mem_divisors, Nat.dvd_prime_pow pp, and_iff_left (ne_of_gt (pow_pos pp.pos k))]

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