Theorems · Definition · group theory

Pi.evalMonoidHom

{I : Type u} → (f : I → Type v) → [inst : (i : I) → MulOneClass (f i)] → (i : I) → ((i : I) → f i) →* f i

Evaluation of functions into an indexed collection of monoids at a point is a monoid homomorphism. This is Function.eval i as a MonoidHom.

Defined in

Mathlib.Algebra.Group.Pi.Lemmas

Cited by

14 results in Mathlib

Foundations

Depth 8 from the axioms · uses Quot.sound

Assumes

MulOneClass