English
The module structure on α can be transported along an additive equivalence e: α ≃+ β to produce a Module A α; i.e., module structure on α is induced from β via e.
Русский
Структура модуля на α может быть перенесена вдоль аддитивного эквивалентности e: α ≃+ β для получения Module A α; то есть структура модуля на α задаётся через β по через e.
LaTeX
$$$\\text{module}(e) : \\text{Module } A \\ α$$$
Lean4
/-- Transport a module instance via an isomorphism of the underlying abelian groups.
This has better definitional properties than `Equiv.module` since here
the abelian group structure remains unmodified. -/
abbrev module (e : α ≃+ β) : Module A α where
toSMul := e.toEquiv.smul A
one_smul := by simp [Equiv.smul_def]
mul_smul := by simp [Equiv.smul_def, mul_smul]
smul_zero := by simp [Equiv.smul_def]
smul_add := by simp [Equiv.smul_def]
add_smul := by simp [Equiv.smul_def, add_smul]
zero_smul := by simp [Equiv.smul_def]
