---

Step * 1 1 2 2 1 1 of Lemma eqmod-by-orbits


1. p : ℕ
2. T : Type
3. u : T List
4. v : T List List
5. p | ||u||
6. (∀orbit∈v.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
7. l_sum(map(λo.||o||;v)) ≡ ||filter(λo.(||o|| =z 1);v)|| mod p
⊢ (||u|| + ||filter(λo.(||o|| =z 1);v)||) ≡ ||filter(λo.(||o|| =z 1);v)|| mod p
BY
{ Assert ⌜||u|| ≡ 0 mod p⌝⋅ }

1
.....assertion..... 
1. p : ℕ
2. T : Type
3. u : T List
4. v : T List List
5. p | ||u||
6. (∀orbit∈v.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
7. l_sum(map(λo.||o||;v)) ≡ ||filter(λo.(||o|| =z 1);v)|| mod p
⊢ ||u|| ≡ 0 mod p

2
1. p : ℕ
2. T : Type
3. u : T List
4. v : T List List
5. p | ||u||
6. (∀orbit∈v.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
7. l_sum(map(λo.||o||;v)) ≡ ||filter(λo.(||o|| =z 1);v)|| mod p
8. ||u|| ≡ 0 mod p
⊢ (||u|| + ||filter(λo.(||o|| =z 1);v)||) ≡ ||filter(λo.(||o|| =z 1);v)|| mod p

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}
2.  T  :  Type
3.  u  :  T  List
4.  v  :  T  List  List
5.  p  |  ||u||
6.  (\mforall{}orbit\mmember{}v.(||orbit||  =  1)  \mvee{}  (p  |  ||orbit||))
7.  l\_sum(map(\mlambda{}o.||o||;v))  \mequiv{}  ||filter(\mlambda{}o.(||o||  =\msubz{}  1);v)||  mod  p
\mvdash{}  (||u||  +  ||filter(\mlambda{}o.(||o||  =\msubz{}  1);v)||)  \mequiv{}  ||filter(\mlambda{}o.(||o||  =\msubz{}  1);v)||  mod  p


By

---

Latex:
Assert  \mkleeneopen{}||u||  \mequiv{}  0  mod  p\mkleeneclose{}\mcdot{}

---

Home Index