Theorems · Theorem · group theory

AddCon.coe_dfinsuppSum

∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M]
  [inst_2 : (i : ι) → Zero (β i)] [inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : AddCon M)
  (h : (i : ι) → β i → M) (f : Π₀ (i : ι), β i), ↑(f.sum h) = f.sum fun i b => ↑(h i b)

Defined in

Mathlib.GroupTheory.Congruence.BigOperators

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqAddCommMonoidZeroDecidable