Theorems · Theorem · ring theory

Pi.evalStarAlgHom_apply

∀ {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) (j : ι) [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] [inst_3 : (i : ι) → Star (A i)] (a : (i : ι) → A i),
  (Pi.evalStarAlgHom R A j) a = (Pi.evalNonUnitalStarAlgHom R A j).toFun a

Defined in

Mathlib.Algebra.Star.StarAlgHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraStar