Theorems · Theorem · general algebraic systems
Finsupp.support_single_subset
∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (fun₀ | a => b).support ⊆ {a}- Defined in
- Mathlib.Data.Finsupp.Single
- Cited by
- 27 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.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- Finsupp.singlestatement · cited by 943
- Finsupp.supportstatement · cited by 828
Cited by27
Results whose statement or proof uses this declaration.
- Finsupp.sum_single_indexproof · cited by 130
- Finsupp.prod_single_indexproof · cited by 26
- Finsupp.mapDomain_supportproof · cited by 10
- Finsupp.single_mem_supportedproof · cited by 5
- AddMonoidAlgebra.support_coeff_mul_subsetproof · cited by 5
- Polynomial.support_monomial_subsetproof · cited by 5
- SkewMonoidAlgebra.support_single_subsetproof · cited by 4
- AddMonoidAlgebra.single_mem_gradeByproof · cited by 4
- MonoidAlgebra.support_coeff_mul_subsetproof · cited by 3
- Finsupp.eq_single_iffproof · cited by 3
- MvPolynomial.support_monomial_subsetproof · cited by 3
- Finsupp.single_le_iffproof · cited by 3