---

Step * of Lemma p-1-mul

∀[p:{2...}]. ∀[a:p-adics(p)].  (a * 1(p) = a ∈ p-adics(p))
BY
{ ((InstLemma `p-adic-ring_wf` [] THEN ParallelLast')
   THEN (MemTypeHD (-1)⋅ THENA Auto)
   THEN Fold `member` (-2)
   THEN (MemTypeHD (-2)⋅ THENA Auto)
   THEN Fold `member` (-3)
   THEN RepUR ``p-adic-ring ring_p group_p monoid_p`` -2
   THEN RepUR ``bilinear assoc ident inverse`` -2
   THEN RepUR ``p-adic-ring comm`` -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:\{2...\}].  \mforall{}[a:p-adics(p)].    (a  *  1(p)  =  a)


By

---

Latex:
((InstLemma  `p-adic-ring\_wf`  []  THEN  ParallelLast')
  THEN  (MemTypeHD  (-1)\mcdot{}  THENA  Auto)
  THEN  Fold  `member`  (-2)
  THEN  (MemTypeHD  (-2)\mcdot{}  THENA  Auto)
  THEN  Fold  `member`  (-3)
  THEN  RepUR  ``p-adic-ring  ring\_p  group\_p  monoid\_p``  -2
  THEN  RepUR  ``bilinear  assoc  ident  inverse``  -2
  THEN  RepUR  ``p-adic-ring  comm``  -1
  THEN  Auto)

---

Home Index