toProdHom — Mathlib

English

The ring structure on 𝓜(𝕜, A) is inherited by pulling back along the injective map toProdMulOpposite.

Русский

Кольцевое строение 𝓜(𝕜, A) задаётся как предобраз через инъекцию toProdMulOpposite.

LaTeX

$$$\\text{instRing}: \\text{Ring}(\\mathcal{M}(\\mathbb{K},A))$ is defined by the pullback along $\\mathrm{toProdMulOpposite}$$$

Lean4

/-- The canonical map `DoubleCentralizer.toProd` as an additive group homomorphism. -/
@[simps]
noncomputable def toProdHom : 𝓜(𝕜, A) →+ (A →L[𝕜] A) × (A →L[𝕜] A)
    where
  toFun := toProd
  map_zero' := rfl
  map_add' _x _y := rfl

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