わり算　その二

任意の実数に対して0以外の逆元の乗法を除法と定める。

x･y⁻¹=z
が除法。yの逆元をかけること。
x･1=z･y
yかけると逆元は消えて乗法単位元(何もしない要素)が現れる関係。乗法においてyを相殺するのがy⁻¹。

また上の式は
x÷y,x･1/yへ変形可能と定める。

乗法の一意性は証明済だが念の為確認。

x･y⁻¹=x･z⁻¹(仮定)
y⁻¹(仮定2)
y⁻¹･1(乗法単位元)
y⁻¹･x･x⁻¹(乗法逆元)
x･y⁻¹･x(乗法交換法則)
(x･y⁻¹)･x⁻¹(乗法結合法則性)
x･z⁻¹･x⁻¹(同値変形)
z⁻¹･x⁻¹･x(乗法交換法則)
z⁻¹･1(乗法逆元)
z⁻¹(乗法単位元)

乗法逆元の演算が一意的であることが示されました。

xを1へ送る乗法の元はx⁻¹だけ。

除法の性質を調べます。

任意の数と1の除法。

1･1=1(乗法単位元)
1･1⁻¹=1(乗法逆元)
1=-1…①

1⁻¹=1¹=1(定義)
1/1=1⁻¹=1…②

x/1=x･1⁻¹=x･1/1=x･1⁻¹=x･1=x(定義と②)

実数を1で割ると変化しません。

除法はこの変形が成立します。
x/1=x·1¯¹=x·1=x

x/yの逆元

x/yを乗法によって1へ送る元。

x/y=x･y⁻¹…①
定義より変形。

(x⁻¹･y)･(x･y⁻¹)(①と単位元の法則)
x･x⁻¹･y･y⁻¹(交換法則)
1･1(逆元)
1(単位元)

よって、x/yの逆元は
x⁻¹･y
y･x⁻¹
y/x

x/yの逆元はy/xが証明されました。
小学校で見た分母分子をひっくり返す形。定義から導けます。

(x·y)･(x·y)¯¹=1(逆元)

(x·y)·(x¯¹·y¯¹)(仮定)
x·x¯¹·y·y¯¹(交換法則)
1·1(逆元)
1(単位元)
(x·y)(x·y)¯¹=(x·y)·x¯¹·y¯¹(一意性)

以上は現時点で定義から演繹できた除法の性質。