English
The associativity of scalar multiplication follows from associativity in the underlying modules.
Русский
Согласование скалярного умножения следует из ассоциативности в базовых модулях.
LaTeX
$$$$ (r s) \\cdot x = r \\cdot (s \\cdot x) $$$$
Lean4
instance colimitModule : Module R (M F) :=
{ colimitMulAction F,
colimitSMulWithZero
F with
smul_add := fun r x y => by
obtain ⟨i, x, rfl⟩ := M.mk_surjective F x
obtain ⟨j, y, rfl⟩ := M.mk_surjective F y
rw [colimit_smul_mk_eq, colimit_smul_mk_eq,
colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j) (IsFiltered.rightToMax i j),
colimit_smul_mk_eq, smul_add,
colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j) (IsFiltered.rightToMax i j),
LinearMap.map_smul, LinearMap.map_smul]
add_smul r s
x := by
obtain ⟨i, x, rfl⟩ := M.mk_surjective F x
simp [_root_.add_smul, colimit_add_mk_eq'] }
