Theorems · Definition · ring theory

Pi.evalNonUnitalStarAlgHom

{ι : Type u_1} →
  (R : Type u_2) →
    (A : ι → Type u_3) →
      (j : ι) →
        [inst : Monoid R] →
          [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] →
            [inst_2 : (i : ι) → DistribMulAction R (A i)] →
              [inst_3 : (i : ι) → Star (A i)] → ((i : ι) → A i) →⋆ₙₐ[R] A j

Function.eval as a NonUnitalStarAlgHom.

Defined in

Mathlib.Algebra.Star.StarAlgHom

Cited by

3 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

MonoidNonUnitalNonAssocSemiringDistribMulActionStar