English
The map fromLocalizedModule' is additive: it preserves addition of localized elements.
Русский
Отображение fromLocalizedModule' сохраняет сложение локализованных элементов.
LaTeX
$$$$ \mathrm{fromLocalizedModule}'(x+y) = \mathrm{fromLocalizedModule}'(x) + \mathrm{fromLocalizedModule}'(y). $$$$
Lean4
theorem fromLocalizedModule'_add (x y : LocalizedModule S M) :
fromLocalizedModule' S f (x + y) = fromLocalizedModule' S f x + fromLocalizedModule' S f y :=
LocalizedModule.induction_on₂
(by
intro a a' b b'
simp only [LocalizedModule.mk_add_mk, fromLocalizedModule'_mk]
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, smul_add, ← map_smul, ← map_smul, ← map_smul, map_add]
congr 1
all_goals rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff']
· simp [mul_smul, Submonoid.smul_def]
· rw [Submonoid.coe_mul, LinearMap.map_smul_of_tower, mul_comm, mul_smul, Submonoid.smul_def])
x y
