sq_of_gcd_eq_one — Mathlib

English

If gcd(a,b) = 1 and ab = c^2, then there exists a0 with a = a0^2 or a = -a0^2.

Русский

Если gcd(a,b) = 1 и ab = c^2, то существует a0 such that a = a0^2 или a = -a0^2.

LaTeX

$$$\\gcd(a,b) = 1 \\land ab = c^2 \\Rightarrow \\exists a_0 \\in \\mathbb{Z},\\ a = a_0^2 \\text{ or } a = -a_0^2$.$$

Lean4

theorem sq_of_gcd_eq_one {a b c : ℤ} (h : Int.gcd a b = 1) (heq : a * b = c ^ 2) : ∃ a0 : ℤ, a = a0 ^ 2 ∨ a = -a0 ^ 2 :=
  by
  have h' : IsUnit (GCDMonoid.gcd a b) := by
    rw [← coe_gcd, h, Int.ofNat_one]
    exact isUnit_one
  obtain ⟨d, ⟨u, hu⟩⟩ := exists_associated_pow_of_mul_eq_pow h' heq
  use d
  rw [← hu]
  rcases Int.units_eq_one_or u with hu' | hu' <;>
    · rw [hu']
      simp

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