exists_eq_pow_of_mul_eq_pow — Mathlib

English

If gcd(a,b) is a unit and a·b = c^k and units are trivial, then a = d^k for some d.

Русский

Если gcd(a,b) единица и a·b = c^k и единицы тривиальны, то существует d, такое что a = d^k.

LaTeX

$$$IsUnit(\\\\gcd a b) \\land (a b = c^k) \\land Subsingleton(Units(\\\\α)) \\Rightarrow \\exists d, a = d^k$$$

Lean4

theorem exists_eq_pow_of_mul_eq_pow [GCDMonoid α] [Subsingleton αˣ] {a b c : α} (hab : IsUnit (gcd a b)) {k : ℕ}
    (h : a * b = c ^ k) : ∃ d : α, a = d ^ k :=
  let ⟨d, hd⟩ := exists_associated_pow_of_mul_eq_pow hab h
  ⟨d, (associated_iff_eq.mp hd).symm⟩

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