English
The evaluation map at index j is a StarAlgHom from the product ∀ i, A i to A j, i.e., it preserves star, addition, and multiplication with respect to the algebra structure over R.
Русский
Отражение оценки в индексе j является StarAlgHom из произведения (∀ i, A i) в A_j, то есть сохраняет операторы звёздной структуры, сложение и умножение в рамках R-алгебр.
LaTeX
$$$ \Pi.evalStarAlgHom : (\forall i, A i) →⋆ₐ[R] A j $$$
Lean4
/-- `Function.eval` as a `StarAlgHom`. -/
@[simps]
def _root_.Pi.evalStarAlgHom (R : Type*) (A : ι → Type*) (j : ι) [CommSemiring R] [∀ i, Semiring (A i)]
[∀ i, Algebra R (A i)] [∀ i, Star (A i)] : (∀ i, A i) →⋆ₐ[R] A j :=
{ Pi.evalNonUnitalStarAlgHom R A j, Pi.evalRingHom A j with commutes' _ := rfl }
