of_pow_associated_of_prime' — Mathlib

English

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

Русский

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

LaTeX

$$$$\mathrm{Prime}(p_1) \land \mathrm{Prime}(p_2) \land 0 < k_2 \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₂ :=
  (h.symm.of_pow_associated_of_prime hp₂ hp₁ hk₂).symm

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