English
The natural injection toProdMulOpposite induces an additive group homomorphism from 𝓜(𝕜,A) to the product of endomorphism spaces.
Русский
Естественное отображение toProdMulOpposite образует гомоморфизм аддитивной группы из 𝓜(𝕜,A) в произведение пространств эндоморфизмов.
LaTeX
$$$\\text{toProdHom}: 𝓜(𝕜,A) \\to^+ (A \\to_L[𝕜] A) \\times (A \\to_L[𝕜] A)$$$
Lean4
/-- The module structure is inherited as the pullback under the additive group monomorphism
`DoubleCentralizer.toProd : 𝓜(𝕜, A) →+ (A →L[𝕜] A) × (A →L[𝕜] A)` -/
noncomputable instance instModule {S : Type*} [Semiring S] [Module S A] [SMulCommClass 𝕜 S A] [ContinuousConstSMul S A]
[IsScalarTower S A A] [SMulCommClass S A A] : Module S 𝓜(𝕜, A) :=
Function.Injective.module S toProdHom (ext (𝕜 := 𝕜) (A := A)) fun _x _y => rfl
