English
An isomorphism of abelian groups e: α ≃+ β transfers an R-module structure from β to α, yielding a canonical Module R α with e as an isomorphism of modules.
Русский
Изоморфизм абелиановых групп e: α ≃+ β переносит R-модульную структуру с β на α, образуя канонический модульный объект R α с e как изоморфизм модулей.
LaTeX
$$$\\text{If } (β, M) \\text{ is an } R\\text{-module and } e: α \\xrightarrow{\\sim} β, \\text{ then } α \\text{ inherits an } R\\text{-module structure making } e$ module isomorphism.$$
Lean4
/-- Transfer `Module` across an `Equiv` -/
protected abbrev module (e : α ≃ β) [AddCommMonoid β] :
let _ := Equiv.addCommMonoid e
∀ [Module R β], Module R α :=
by
intros
exact
({ Equiv.distribMulAction R e with
zero_smul := by simp [smul_def, zero_smul, zero_def]
add_smul := by simp [add_def, smul_def, add_smul] } :
Module R α)
