Theorems · Theorem · group theory

MonoidHom.functions_ext

∀ {I : Type u_7} [inst : DecidableEq I] {M : I → Type u_8} [inst_1 : (i : I) → CommMonoid (M i)] [Finite I]
  (N : Type u_9) [inst_3 : CommMonoid N] (g h : ((i : I) → M i) →* N),
  (∀ (i : I) (x : M i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)) → g = h

Defined in

Mathlib.Algebra.BigOperators.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqCommMonoidFiniteCommMonoid