exists_associated_pow_of_mul_eq_pow'

English

If a and b are coprime and ab equals c^k, then there exists d such that d^k is associated to a.

Русский

Если a и b взаимно просты и произведение ab равно c^k, то существует d, такое что d^k ассоциировано с a.

LaTeX

$$$\forall {R} [\mathrm{CommRing}\,R] [IsBezout R] {a b c : R} (hab : \mathrm{IsCoprime}\,a\,b) {k : \mathbb{N}} (h : a \cdot b = c^k) : \exists d : R, \mathrm{Associated}(d^k,a)$$$

Lean4

theorem exists_associated_pow_of_mul_eq_pow' {a b c : R} (hab : IsCoprime a b) {k : ℕ} (h : a * b = c ^ k) :
    ∃ d : R, Associated (d ^ k) a := by
  classical
  letI := IsBezout.toGCDDomain R
  exact exists_associated_pow_of_mul_eq_pow ((gcd_isUnit_iff _ _).mpr hab) h

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