Theorems · Definition · group theory

MonoidHom.mulSingle

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

The monoid homomorphism including a single monoid into a dependent family of additive monoids, as functions supported at a point. This is the MonoidHom version of Pi.mulSingle.

Defined in

Mathlib.Algebra.Group.Pi.Lemmas

Cited by

21 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqMulOneClass