English
DivisibleHull M carries a module structure over the rational numbers, with scalar multiplication defined compatibly with addition and multiplication of rationals.
Русский
DivisibleHull M имеет структуру модуля над рационалами, скаляльное умножение совместимо со сложением и умножением рациональных чисел.
LaTeX
$$$\\mathrm{DivisibleHull}(M)$ is a module over $\\mathbb{Q}$.$$
Lean4
noncomputable instance : Module ℚ (DivisibleHull M)
where
one_smul
x :=
by
induction x with
| mk m s
simp [qsmul_of_nonneg zero_le_one, nnqsmul_mk]
zero_smul := zero_qsmul
smul_zero a := by simp [qsmul_def]
smul_add a x y := by simp [qsmul_def, smul_add]
add_smul a b
x :=
by
induction x with
| mk m s
simp_rw [qsmul_mk, mk_add_mk, mk_eq_mk]
use 1
suffices ((a + b).num * a.den * b.den * (s * s)) • m = ((a.num * b.den + b.num * a.den) * (a + b).den * (s * s)) • m
by
convert this using 1
all_goals
simp [← natCast_zsmul, smul_smul, ← add_smul]
ring_nf
rw [Rat.add_num_den']
mul_smul a b
x :=
by
induction x with
| mk m s
simp_rw [qsmul_mk, mk_eq_mk]
use 1
suffices ((a * b).num * a.den * b.den * s) • m = (a.num * b.num * (a * b).den * s) • m
by
convert this using 1
all_goals
simp [← natCast_zsmul, smul_smul]
ring_nf
rw [Rat.mul_num_den']
