---

Step * of Lemma residues-equal-bags

∀n:{2...}. ∀a:ℕ+.  (CoPrime(n,a) ⇒ (map(λi.(ai mod n);residues-mod(n)) = residues-mod(n) ∈ bag(residue(n))))
BY
{ (Auto THEN EqTypeD 0 THEN Auto THEN Try ((DVar `i' THEN Unhide THEN Auto)) THEN BLemma `residues-permute` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\{2...\}.  \mforall{}a:\mBbbN{}\msupplus{}.    (CoPrime(n,a)  {}\mRightarrow{}  (map(\mlambda{}i.(ai  mod  n);residues-mod(n))  =  residues-mod(n)))


By

---

Latex:
(Auto
  THEN  EqTypeD  0
  THEN  Auto
  THEN  Try  ((DVar  `i'  THEN  Unhide  THEN  Auto))
  THEN  BLemma  `residues-permute`
  THEN  Auto)

---

Home Index