English
If −1 is a square modulo coprime natural numbers m and n, then −1 is a square modulo m n.
Русский
Если −1 является квадратом по модулю coprime чисел m и n, тогда −1 является квадратом по модулю mn.
LaTeX
$$$ \forall m,n \in \mathbb{N},\ \gcd(m,n)=1 \rightarrow IsSquare(-1 : \mathbb{Z}/m\mathbb{Z}) \rightarrow IsSquare(-1 : \mathbb{Z}/n\mathbb{Z}) \rightarrow IsSquare(-1 : \mathbb{Z}/(m n)\mathbb{Z})$$$
Lean4
/-- If `-1` is a square modulo coprime natural numbers `m` and `n`, then `-1` is also
a square modulo `m*n`. -/
theorem isSquare_neg_one_mul {m n : ℕ} (hc : m.Coprime n) (hm : IsSquare (-1 : ZMod m)) (hn : IsSquare (-1 : ZMod n)) :
IsSquare (-1 : ZMod (m * n)) :=
by
have : IsSquare (-1 : ZMod m × ZMod n) :=
by
rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]
obtain ⟨x, hx⟩ := hm
obtain ⟨y, hy⟩ := hn
rw [hx, hy]
exact ⟨(x, y), rfl⟩
simpa only [RingEquiv.map_neg_one] using this.map (ZMod.chineseRemainder hc).symm
