sq_of_isCoprime — Mathlib

English

If a and b are coprime and ab = c^2, then there exists a0 with a = a0^2 or a = -a0^2.

Русский

Если a и b взаимно просты и ab = c^2, то существует a0, такое что a = a0^2 или a = -a0^2.

LaTeX

$$$\\text{If } \\text{IsCoprime}(a,b) \\land ab = c^2, \\text{ then } \\exists a_0: \\mathbb{Z},\\ a = a_0^2 \\text{ or } a = -a_0^2.$$$

Lean4

theorem sq_of_isCoprime {a b c : ℤ} (h : IsCoprime a b) (heq : a * b = c ^ 2) : ∃ a0 : ℤ, a = a0 ^ 2 ∨ a = -a0 ^ 2 :=
  sq_of_gcd_eq_one (isCoprime_iff_gcd_eq_one.mp h) heq

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