mkOfSMul — Mathlib

English

The object mkOfSMul φ is the module obtained by taking the underlying abelian group A and equipping it with the scalar action provided by φ, i.e., it is the module object (ModuleCat.mkOfSMul' φ) seen as ModuleCat R via ModuleCat.of.

Русский

Объект mkOfSMul φ есть модуль над R, получаемый из базовой абелевой группы A с действием скаляров через φ.

LaTeX

$$$\mathrm{mkOfSMul}(\phi) = \mathrm{ModuleCat.of}(R, \mathrm{mkOfSMul}'\phi)$.$$

Lean4

/-- Given `A : AddCommGrpCat` and a ring morphism `R →+* End A`, this is an object in
`ModuleCat R`, whose underlying abelian group is `A` and whose scalar multiplication is
given by `R`. -/
abbrev mkOfSMul :=
  ModuleCat.of R (mkOfSMul' φ)

Похожие утверждения