---

Step * 1 of Lemma quadratic-residue_functionality


1. a : ℤ@i
2. a' : ℤ@i
3. p : ℤ@i
4. a' ≡ a mod p@i
⊢ a' is a quadratic residue mod p ⇐⇒ a is a quadratic residue mod p
BY
{ (Unfold `quadratic-residue` 0 THEN RWO "4" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}@i
2.  a'  :  \mBbbZ{}@i
3.  p  :  \mBbbZ{}@i
4.  a'  \mequiv{}  a  mod  p@i
\mvdash{}  a'  is  a  quadratic  residue  mod  p  \mLeftarrow{}{}\mRightarrow{}  a  is  a  quadratic  residue  mod  p


By

---

Latex:
(Unfold  `quadratic-residue`  0  THEN  RWO  "4"  0  THEN  Auto)

---

Home Index