Theorems · Theorem · general algebraic systems
Finsupp.mapDomain_support
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : DecidableEq β] {f : α → β}
{s : α →₀ M}, (Finsupp.mapDomain f s).support ⊆ Finset.image f s.support- Defined in
- Mathlib.Data.Finsupp.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoidDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finsuppstatement and proof · cited by 5,255
- le_reflproof · cited by 2,061
- Finset.imagestatement and proof · cited by 910
- Finsupp.supportstatement and proof · cited by 828
- Finsupp.mapDomainstatement · cited by 168
- Finsupp.support_single_subsetproof · cited by 27
- Finset.Subset.transproof · cited by 18
- Finsupp.support_sumproof · cited by 7
- Finset.biUnion_monoproof · cited by 3
- Finset.biUnion_singletonproof · cited by 2
Cited by10
Results whose statement or proof uses this declaration.
- MvPolynomial.coeff_rename_eq_zeroproof · cited by 3
- Finsupp.lmapDomain_supportedproof · cited by 2
- MvPolynomial.totalDegree_rename_leproof · cited by 2
- MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_leproof · cited by 1
- MvPolynomial.coeff_killComplproof · cited by 1
- Convexity.IsConvexSet.iConvexComb_memproof · cited by 1
- Finsupp.mapDomain_support_of_injOnproof · cited by 1
- Finsupp.supported_comap_lmapDomainproof · cited by 1
- Convexity.IsConvexSet.piproof · cited by 0
- Convexity.IsConvexSet.prodproof · cited by 0