---

Step * 1 1 of Lemma fermat-little


1. p : ℕ
2. prime(p)
3. x : ℕ
4. ℕp ⟶ ℕx ~ ℕx^p
⊢ Inj(ℕp ⟶ ℕx;ℕp ⟶ ℕx;λg.(g o rot(p)))
BY
{ TACTIC:((D 0 THEN Reduce 0) THEN Auto) }

1
1. p : ℕ
2. prime(p)
3. x : ℕ
4. ℕp ⟶ ℕx ~ ℕx^p
5. a1 : ℕp ⟶ ℕx
6. a2 : ℕp ⟶ ℕx
7. (a1 o rot(p)) = (a2 o rot(p)) ∈ (ℕp ⟶ ℕx)
⊢ a1 = a2 ∈ (ℕp ⟶ ℕx)

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}
2.  prime(p)
3.  x  :  \mBbbN{}
4.  \mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x  \msim{}  \mBbbN{}x\^{}p
\mvdash{}  Inj(\mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x;\mBbbN{}p  {}\mrightarrow{}  \mBbbN{}x;\mlambda{}g.(g  o  rot(p)))


By

---

Latex:
TACTIC:((D  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index