Theorems · Theorem · group theory

AddMonoidHom.functions_ext

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

Defined in

Mathlib.Algebra.BigOperators.Pi

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidableEqAddCommMonoidFiniteAddCommMonoid