Theorems · Theorem · group theory
AddCon.coe_dfinsuppSumAddHom
∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M]
[inst_2 : (i : ι) → AddCommMonoid (β i)] (c : AddCon M) (h : (i : ι) → β i →+ M) (f : Π₀ (i : ι), β i),
↑((DFinsupp.sumAddHom h) f) = (DFinsupp.sumAddHom fun i => c.mk'.comp (h i)) f- Cited by
- 1 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- AddCommMonoidstatement and proof · cited by 12,281
- AddMonoidHomstatement and proof · cited by 3,230
- DFinsuppstatement and proof · cited by 694
- AddMonoidHom.compstatement and proof · cited by 339
- AddConstatement and proof · cited by 138
- DFinsupp.sumproof · cited by 64
- AddCon.Quotientstatement · cited by 54
- AddCon.toQuotientstatement · cited by 38
- DFinsupp.sumAddHomstatement · cited by 38
- AddCon.mk'statement and proof · cited by 21
- DFinsupp.sumAddHom_applyproof · cited by 16
Cited by1
Results whose statement or proof uses this declaration.
- RingCon.coe_dfinsuppSumAddHomproof · cited by 0