unit_mul_pow_congr_pow — Mathlib

English

If p and q are irreducible and u, v are units with u p^m = v q^n, then m = n.

Русский

Если p и q ирредуцируемы, а u, v — единицы, и u p^m = v q^n, то m = n.

LaTeX

$$$m = n$$$

Lean4

theorem unit_mul_pow_congr_pow {p q : R} (hp : Irreducible p) (hq : Irreducible q) (u v : Rˣ) (m n : ℕ)
    (h : ↑u * p ^ m = v * q ^ n) : m = n :=
  by
  have key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod :=
    by
    rw [Multiset.prod_replicate, Multiset.prod_replicate, Associated]
    refine ⟨u * v⁻¹, ?_⟩
    simp only [Units.val_mul]
    rw [mul_left_comm, ← mul_assoc, h, mul_right_comm, Units.mul_inv, one_mul]
  have := by
    refine Multiset.card_eq_card_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ key)
    all_goals
      intro x hx
      obtain rfl := Multiset.eq_of_mem_replicate hx
      assumption
  simpa only [Multiset.card_replicate]

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