[Coq][Math] From left unit and left inverse to right unit and inverse

群で左単位元と左逆元があれば、右単位元と右逆元があることの説明。

Coq 演習で、Coq 以外のところで行き詰まっていた人がいたので参考になればと。

逆元と単位元の導入/除去のとこだけ詳しく書きますが、結合則使って演算順序を変えるところは各自 rewrite とかで頑張ってください。

$x 1 = 1 x 1 = \{(x^{-1})^{-1} x^{-1}\} x (x^{-1}x) = (x^{-1})^{-1} (x^{-1}x) x^{-1}x$
$= (x^{-1})^{-1} 1 x^{-1} x = (x^{-1})^{-1} x^{-1} x = \{ (x^{-1})^{-1} x^{-1}\} x = 1 x = x$

$x x^{-1} = 1 x x^{-1} = \{ (x^{-1})^{-1} x^{-1} \} x x^{-1}$
$= (x^{-1})^{-1} (x^{-1}x) x^{-1} = (x^{-1})^{-1}  1  x^{-1}$
$= (x^{-1})^{-1} (1 x^{-1}) = (x^{-1})^{-1} x^{-1} = 1$

[IVA] Chapter 1, Section 1, Exercise 4

Ideals, Varieties, and Algorithms の演習問題。

Chapter1, Section 1, Exersise 4: Let $F$ be a finite field with $q$ elements.  Adapt the argument of Exersise 3 to prove that $x^q - x$ is a nonzero polynomial in $F\left[x\right]$ which vanishes at every point of $F$.  This shows that Proposition 5 fails for all finite fields.

解答：
$F$ は要素数 $q$ の有限体であるから、$F - \left\{0\right\}$ は要素数 $q - 1$ の有限群となることは、体の定義より明らか。
$F - \left\{0\right\}$ の任意の要素 $x$ に対して、$x$ の位数が $q - 1$ の約数であることはラグランジュの定理より明らか。
すると前問 3b より、$x \neq 0$ ならば $x^{q-1} = 1$ より $x^q - x = 0$.
同様に $x = 0$ なら $x^q - x = 0$.
よって全ての $x \in F$ に対して $f(x) = x^q - x \; \in \; F_p\left[x\right]$ は零となる。