Theorems · Definition · general algebraic systems
Finsupp.sumElim
{α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → [inst : Zero γ] → (α →₀ γ) → (β →₀ γ) → α ⊕ β →₀ γFinsupp.sumElim f g maps inl x to f x and inr y to g y.
- Defined in
- Mathlib.Data.Finsupp.Basic
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Zero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsuppstatement and proof · cited by 5,255
- Finsupp.supportproof · cited by 828
- Finset.disjSumproof · cited by 55
Cited by26
Results whose statement or proof uses this declaration.
- Finsupp.sumFinsuppAddEquivProdFinsupp_symm_applystatement · cited by 10
- Finsupp.sumFinsuppEquivProdFinsuppproof · cited by 6
- Finsupp.sumElim_zero_zerostatement · cited by 4
- Finsupp.sumElim_zero_singlestatement · cited by 3
- Finsupp.sumElim_single_zerostatement · cited by 2
- Finsupp.sumElim_supportstatement and proof · cited by 2
- Finsupp.sumElim_addstatement · cited by 1
- Finsupp.sumElim_eq_addstatement · cited by 1
- Finsupp.sumElim_single_singlestatement · cited by 1
- Algebra.Generators.ofComp_toAlgHom_monomial_sumElimstatement and proof · cited by 1
- Finsupp.comapDomain_inl_sumElimstatement · cited by 1
- Finsupp.comapDomain_inr_sumElimstatement · cited by 1