---

Step * of Lemma int_op_minus

∀[g:Group{i}]. ∀[e:|g|]. ∀[a:ℤ].  (-a x(*;e;~) e = (~ a x(*;e;~) e) ∈ |g|)
BY
{ UnivCD THENA Auto }

1
1. g : Group{i}
2. e : |g|
3. a : ℤ
⊢ -a x(*;e;~) e = (~ a x(*;e;~) e) ∈ |g|

---

Latex:

---

Latex:
\mforall{}[g:Group\{i\}].  \mforall{}[e:|g|].  \mforall{}[a:\mBbbZ{}].    (-a  x(*;e;\msim{})  e  =  (\msim{}  a  x(*;e;\msim{})  e))


By

---

Latex:
UnivCD  THENA  Auto

---

Home Index