eq_pow_of_mul_eq_pow_odd — Mathlib

English

If a and b are coprime and a b = c^k with k odd, then both a and b are k-th powers: a = d^k and b = e^k.

Русский

Если a и b взаимно просты и ab = c^k с нечетным k, то оба числа являются k-й степенной степенью: a = d^k, b = e^k.

LaTeX

$$$\\text{IsCoprime}(a,b) \\Rightarrow (\\exists d: \\mathbb{Z}, a = d^k) \\land (\\exists e: \\mathbb{Z}, b = e^k).$$$

Lean4

theorem eq_pow_of_mul_eq_pow_odd {a b c : ℤ} (hab : IsCoprime a b) {k : ℕ} (hk : Odd k) (h : a * b = c ^ k) :
    (∃ d, a = d ^ k) ∧ ∃ e, b = e ^ k :=
  ⟨eq_pow_of_mul_eq_pow_odd_left hab hk h, eq_pow_of_mul_eq_pow_odd_right hab hk h⟩

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