---

Step * of Lemma perm_grp_inv_thru_op

∀[T:Type]. ∀[a,b:Perm(T)].  (inv_perm(a O b) = inv_perm(b) O inv_perm(a) ∈ Perm(T))
BY
{ (ProveSpecializedLemma `grp_inv_thru_op` 1 [parm{i}; perm_igrp(T)] (AbReduceC)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a,b:Perm(T)].    (inv\_perm(a  O  b)  =  inv\_perm(b)  O  inv\_perm(a))


By

---

Latex:
(ProveSpecializedLemma  `grp\_inv\_thru\_op`  1  [parm\{i\};  perm\_igrp(T)]  (AbReduceC))

---

Home Index