dvd_prime_pow — Mathlib

English

Let p be prime. i ∣ p^m ↔ ∃ k ≤ m, i = p^k.

Русский

Пусть p — простое. i делит p^m тогда и только тогда, когда ∃ k ≤ m, i = p^k.

LaTeX

$$$$ \forall p \in \mathbb{N},\text{Prime}(p) \rightarrow \forall m,i \in \mathbb{N},\ i \mid p^m \iff \exists k \le m, i = p^k. $$$$

Lean4

theorem dvd_prime_pow {p : ℕ} (pp : Prime p) {m i : ℕ} : i ∣ p ^ m ↔ ∃ k ≤ m, i = p ^ k := by
  simp_rw [_root_.dvd_prime_pow (prime_iff.mp pp) m, associated_eq_eq]

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