Theorems · Definition · ring theory

Pi.evalAlgHom

{ι : Type u_1} →
  (R : Type u_2) →
    (A : ι → Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A i)] → [inst_2 : (i : ι) → Algebra R (A i)] → (i : ι) → ((i : ι) → A i) →ₐ[R] A i

Function.eval as an AlgHom. The name matches Pi.evalRingHom, Pi.evalMonoidHom, etc.

Defined in

Mathlib.Algebra.Algebra.Pi

Cited by

13 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebra