公理主義実数論の立場から除法≒割り算を考えます。

除法

実数 x の正整数 n 乗は、素朴には、n 個の x を掛け合わせたものである。厳密には、次のように再帰的に定められる。
(∗)x¹:=x,
(∗∗)xn+1:=xⁿ×x(n≥1)
.x0 を定義する場合には、関係式 (∗∗) が n = 0 でも成立するように定義を拡張するのが自然である。
ウィキペディア

除法

x･y=z(仮定)
x･y・y⁻¹=z･y⁻¹(同値変形)
x･1=z･y⁻¹(乗法逆元)
x=z･y⁻¹(乗法単位元)

x=z･y⁻¹=z･1/y=z÷y

この文脈が除法。

y¹を相殺し1に変形するのがy¹の逆元y⁻¹。
n乗の定義を踏まえればy⁻¹=1/yの同値関係が除法であると定義できます。
あるいはx･y=z⇔x=z･y⁻¹が乗法と除法の関係。

例
2¹･2⁻¹=2/1･1/2=2･0.5=1

10¹･10⁻¹=10･1･1/10=10･01=1

この関係
x･y=z⇔y=z･x⁻¹

よく中学生か高校で目にした変形。

x実数 x の正整数 n 乗は、素朴には、n 個の x を掛け合わせたものである。厳密には、次のように再帰的に定められる。
(∗)x1:=x,
(∗∗)xn+1:=xn×x(n≥1)
ウィキペディア

練習問題

1･1=1(除法単位元)
1･1⁻¹=1(乗法逆元)
1⁻¹･1=1(交換律)
1⁻¹=1(乗法一意性.)…①

x･1⁻¹=x/1
と定義②。

x(仮定)
x･1(乗法単位元)
x･1⁻¹(①)
x/1(②)
x⇔x･1⇔x･1⁻¹⇔x/1

x⁻¹=1/xと定義
x･x⁻¹=1
x･1/x=1

-1乗で分数を表現できます。

乗法一意性

自明にみえますが、年のために乗法の一意性が成り立つのかを確認します。

x･y=x･z(前提)
y(仮定)
y･(x･x⁻¹)(乗法逆元)
(y･x)･x⁻¹(乗法結合律)
(x･y)･x⁻¹(乗法交換律)
(x･z)･x⁻¹(同値関係)
(z･x)･x⁻¹(乗法交換律)
z･(x･x⁻¹)(乗法結合律)
z･1(乗法逆元)
z(乗法単位元)
x･y=x･z→y=z

逆も真なのでz→y。すなわちz=y。

練習問題

(x ･y)¹(x⁻¹･y⁻¹)⁻=1
の証明

(x･y )¹･(x⁻¹･y⁻¹)(仮定)
(x･x⁻¹)･(y¹･y⁻¹)(乗法交換律)
1･1(乗法逆元)
1(乗法単位元)
((x･y )¹･(x⁻¹･y⁻¹)→1)∧((x･y )¹･(x･y)⁻¹→1)(∧導入)
(x⁻¹･y⁻¹)=(x･y)⁻¹(乗法一意性)