eq_of_prime_pow_eq — Mathlib

English

If p1 and p2 are primes in a cancellative monoid with zero, and k1>0, and p1^k1 = p2^k2, then p1 = p2.

Русский

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

LaTeX

$$$$\forall R,[\mathrm{CancelCommMonoidWithZero}\, R], \mathrm{Subsingleton}(\mathrm{Units}\, R) \, \Rightarrow \, \mathrm{Prime}(p_1) \land \mathrm{Prime}(p_2) \land 0 < k_1 \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₁

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