toAddMonoidHom_proj — Mathlib

English

The pi construction defines a linear map into the space of functions i ↦ φ_i, coordinatewise linear.

Русский

Конструкция Pi задаёт линейное отображение в пространство функций i ↦ φ_i, координатно линейное.

LaTeX

$$pi : (i ↦ M₂ →ₗ φ i) → M₂ →ₗ (i ↦ φ i)$$

Lean4

@[simp]
theorem toAddMonoidHom_proj (i : ι) : (proj i).toAddMonoidHom (R := R) = Pi.evalAddMonoidHom φ i :=
  rfl

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