eq_pow_of_mul_eq_pow_odd_left — Mathlib

English

Let a,b be coprime. If a b = c^k with k odd, then a is a k-th power: a = d^k for some d ∈ ℤ.

Русский

Пусть a и b взаимно просты. Если a b = c^k и k нечетно, то a есть k-я степенная степень: a = d^k для некоторого d.

LaTeX

$$$\\text{IsCoprime}(a,b) \\Rightarrow \\forall k\\; (\\text{Odd}(k) \\Rightarrow a b = c^k \\Rightarrow \\exists d: \\mathbb{Z}, a = d^k).$$$

Lean4

theorem eq_pow_of_mul_eq_pow_odd_left {a b c : ℤ} (hab : IsCoprime a b) {k : ℕ} (hk : Odd k) (h : a * b = c ^ k) :
    ∃ d, a = d ^ k := by
  obtain ⟨d, hd⟩ := exists_associated_pow_of_mul_eq_pow' hab h
  replace hd := hd.symm
  rw [associated_iff_natAbs, natAbs_eq_natAbs_iff, ← hk.neg_pow] at hd
  obtain rfl | rfl := hd <;> exact ⟨_, rfl⟩

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