evalNonUnitalStarAlgHom — Mathlib

English

For a family (A i) indexed by i ∈ ι, the evaluation map at index j, taking a family (a i) to a j, defines a nonunital star algebra homomorphism from the product ∀i, A i to A j.

Русский

Для семейства (A_i) индексируемого по i∈ι, отображение оценки в индексе j, отдающее последовательность (a_i) в элемент a_j, задаёт неполный звёздно-алгебра-гомоморфизм из произведения (∀ i, A_i) в A_j.

LaTeX

$$$ \Pi.evalNonUnitalStarAlgHom : (\forall i, A i) →⋆ₙₐ[R] A j $$$

Lean4

/-- `Function.eval` as a `NonUnitalStarAlgHom`. -/
@[simps]
def _root_.Pi.evalNonUnitalStarAlgHom (R : Type*) (A : ι → Type*) (j : ι) [Monoid R]
    [∀ i, NonUnitalNonAssocSemiring (A i)] [∀ i, DistribMulAction R (A i)] [∀ i, Star (A i)] : (∀ i, A i) →⋆ₙₐ[R] A j :=
  { Pi.evalMulHom A j, Pi.evalAddHom A j with
    map_smul' _ _ := rfl
    map_zero' := rfl
    map_star' _ := rfl }

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