exists_associated_pow_of_associated_pow_mul

English

If a and b are coprime and c^k is associated to a b, then there exists d with d^k associated to a.

Русский

Если a и b взаимно просты, и c^k ассоциировано с a b, то существует 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 : \mathrm{Associated}(c^k, a b)) : \exists d : R, \mathrm{Associated}(d^k, a)$$$

Lean4

theorem exists_associated_pow_of_associated_pow_mul {a b c : R} (hab : IsCoprime a b) {k : ℕ}
    (h : Associated (c ^ k) (a * b)) : ∃ d : R, Associated (d ^ k) a :=
  by
  obtain ⟨u, hu⟩ := h.symm
  exact
    exists_associated_pow_of_mul_eq_pow' ((isCoprime_mul_unit_right_right u.isUnit a b).mpr hab) <| mul_assoc a _ _ ▸ hu

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