Step
*
of Lemma
residues-mod_wf
∀[n:ℕ]. (residues-mod(n) ∈ residue(n) List)
BY
{ (Auto THEN Unfold `residues-mod` 0) }
1
1. n : ℕ
⊢ filter(λi.(gcd(n;i) =z 1);upto(n)) ∈ residue(n) List
Latex:
Latex:
\mforall{}[n:\mBbbN{}]. (residues-mod(n) \mmember{} residue(n) List)
By
Latex:
(Auto THEN Unfold `residues-mod` 0)
Home
Index