evalAlgHom — Mathlib

English

Evaluation at a fixed index i yields an algebra homomorphism from the product to A_i.

Русский

Оценка по фиксированному индексу i даёт алгебрный гомоморфизм из произведения в A_i.

LaTeX

$$$ evalAlgHom_i: (\\Pi i, A_i) \\to_{Alg,R} A_i $$$

Lean4

/-- `Function.eval` as an `AlgHom`. The name matches `Pi.evalRingHom`, `Pi.evalMonoidHom`,
etc. -/
@[simps]
def evalAlgHom (i : ι) : (Π i, A i) →ₐ[R] A i :=
  { Pi.evalRingHom A i with
    toFun := fun f ↦ f i
    commutes' := fun _ ↦ rfl }

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