Theorems · Theorem · group theory

RingHom.functions_ext

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

Defined in

Mathlib.Algebra.BigOperators.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqNonAssocSemiringFiniteNonAssocSemiring