of_pow_associated_of_prime — Mathlib

English

If p1 and p2 are prime, k1>0, and p1^k1 is associated to p2^k2, then p1 is associated to p2.

Русский

Если p1, p2 — простые, k1>0 и p1^k1 ассоциировано с p2^k2, то p1 ассоциировано с p2.

LaTeX

$$$$\mathrm{Prime}(p_1) \land \mathrm{Prime}(p_2) \land 0 < k_1 \land p_1^{k_1} \sim_{\mathrm{a}} p_2^{k_2} \Rightarrow p_1 \sim_{\mathrm{a}} p_2.$$$$

Lean4

theorem of_pow_associated_of_prime [CancelCommMonoidWithZero M] {p₁ p₂ : M} {k₁ k₂ : ℕ} (hp₁ : Prime p₁)
    (hp₂ : Prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ ~ᵤ p₂ ^ k₂) : p₁ ~ᵤ p₂ :=
  by
  have : p₁ ∣ p₂ ^ k₂ := by
    rw [← h.dvd_iff_dvd_right]
    apply dvd_pow_self _ hk₁.ne'
  rw [← hp₁.dvd_prime_iff_associated hp₂]
  exact hp₁.dvd_of_dvd_pow this

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