eq_of_prime_pow_eq' — Mathlib

English

If p1 and p2 are primes, hk2 > 0, and p1^k1 = p2^k2, then p1 = p2.

Русский

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

LaTeX

$$$$\forall R,[\mathrm{CancelCommMonoidWithZero}\, R], \mathrm{Prime}(p_1) \land \mathrm{Prime}(p_2) \land 0 < k_2 \land p_1^{k_1} = p_2^{k_2} \Rightarrow p_1 = p_2.$$$$

Lean4

theorem eq_of_prime_pow_eq' (hp₁ : Prime p₁) (hp₂ : Prime p₂) (hk₁ : 0 < k₂) (h : p₁ ^ k₁ = p₂ ^ k₂) : p₁ = p₂ :=
  by
  rw [← associated_iff_eq] at h ⊢
  apply h.of_pow_associated_of_prime' hp₁ hp₂ hk₁

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