Theorems · Definition · general algebraic systems
DFinsupp.liftAddHom
{ι : Type u} →
{γ : Type w} →
{β : ι → Type v} →
[DecidableEq ι] →
[inst : (i : ι) → AddZeroClass (β i)] →
[inst_1 : AddCommMonoid γ] → ((i : ι) → β i →+ γ) ≃+ ((Π₀ (i : ι), β i) →+ γ)The DFinsupp version of Finsupp.liftAddHom
- Defined in
- Mathlib.Data.DFinsupp.BigOperators
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommMonoidstatement and proof · cited by 12,281
- AddMonoidHomstatement and proof · cited by 3,230
- AddZeroClassstatement and proof · cited by 1,237
- AddEquivstatement · cited by 1,087
- DFinsuppstatement and proof · cited by 694
- AddMonoidHom.compproof · cited by 339
- DFinsupp.sumAddHomproof · cited by 38
- DFinsupp.singleAddHomproof · cited by 17
Cited by12
Results whose statement or proof uses this declaration.
- DirectSum.toAddMonoidproof · cited by 11
- DFinsupp.liftAddHom_applystatement and proof · cited by 6
- DFinsupp.sum_singleproof · cited by 4
- DFinsupp.comp_liftAddHomstatement and proof · cited by 4
- DFinsupp.liftAddHom_singleAddHomstatement and proof · cited by 2
- DirectSum.toAddMonoid_injectiveproof · cited by 2
- DFinsupp.liftAddHom_apply_singlestatement · cited by 1
- DFinsupp.liftAddHom_comp_singlestatement · cited by 1
- DFinsupp.liftAddHom_symm_applystatement and proof · cited by 1
- DFinsupp.sum_sub_indexproof · cited by 0
- DFinsupp.sumAddHom_addproof · cited by 0
- DFinsupp.sumAddHom_zeroproof · cited by 0