Theorems · Theorem · group theory

AddMonoidHom.noncommPiCoprod_single

∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → AddMonoid (N i)] (ϕ : (i : ι) → N i →+ M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)} [inst_3 : DecidableEq ι] (i : ι)
  (y : N i), (AddMonoidHom.noncommPiCoprod ϕ hcomm) (Pi.single i y) = (ϕ i) y

Defined in

Mathlib.GroupTheory.NoncommPiCoprod

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddMonoidFintypeAddMonoidDecidableEq