isSquare_neg_one_of_dvd — Mathlib

English

If −1 is a square modulo n and m divides n, then −1 is also a square modulo m.

Русский

Если −1 является квадратом по модулю n и m делит n, то −1 также является квадратом по модулю m.

LaTeX

$$$ \forall m,n \in \mathbb{N},\ m \mid n \rightarrow IsSquare(-1 : \mathbb{Z}/n\mathbb{Z}) \rightarrow IsSquare(-1 : \mathbb{Z}/m\mathbb{Z})$$$

Lean4

/-- If `-1` is a square modulo `n` and `m` divides `n`, then `-1` is also a square modulo `m`. -/
theorem isSquare_neg_one_of_dvd {m n : ℕ} (hd : m ∣ n) (hs : IsSquare (-1 : ZMod n)) : IsSquare (-1 : ZMod m) :=
  by
  let f : ZMod n →+* ZMod m := ZMod.castHom hd _
  rw [← RingHom.map_one f, ← RingHom.map_neg]
  exact hs.map f

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