eq_pow_of_mul_eq_pow_odd_right — Mathlib

English

Symmetric version: if a,b are coprime and a b = c^k with k odd, then b is a k-th power.

Русский

Зеркальная версия: если a и b взаимно просты и ab = c^k с нечетным k, то b = e^k для некоторого e.

LaTeX

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

Lean4

theorem eq_pow_of_mul_eq_pow_odd_right {a b c : ℤ} (hab : IsCoprime a b) {k : ℕ} (hk : Odd k) (h : a * b = c ^ k) :
    ∃ d, b = d ^ k :=
  eq_pow_of_mul_eq_pow_odd_left (c := c) hab.symm hk (by rwa [mul_comm] at h)

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