prodMapAlgHom — Mathlib

English

The right-inclusion map preserves multiplication: inr(b1 b2) = inr(b1) · inr(b2).

Русский

Правый инклюзив сохраняет умножение: inr(b1 b2) = inr(b1) · inr(b2).

LaTeX

$$$ \\text{inr }(b_1 b_2) = \\text{inr }(b_1) \\cdot \\text{inr }(b_2). $$$

Lean4

/-- `LinearMap.prodMap` as an `AlgHom` -/
@[simps!]
def prodMapAlgHom : Module.End R M × Module.End R M₂ →ₐ[R] Module.End R (M × M₂) :=
  { prodMapRingHom R M M₂ with commutes' := fun _ => rfl }

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