Theorems · Theorem · general algebraic systems
Finsupp.mapDomain_comapDomain
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α → β) (hf : Function.Injective f)
(l : β →₀ M), ↑l.support ⊆ Set.range f → Finsupp.mapDomain f (Finsupp.comapDomain f l ⋯) = l- Defined in
- Mathlib.Data.Finsupp.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setstatement · cited by 53,352
- Finsetstatement · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- SetLike.coestatement and proof · cited by 8,199
- Finsuppstatement and proof · cited by 5,255
- Set.preimagestatement · cited by 4,946
- Set.rangestatement and proof · cited by 4,705
- Finsupp.supportstatement and proof · cited by 828
- Function.Injective.injOnstatement and proof · cited by 280
- Finsupp.mapDomainstatement and proof · cited by 168
- Function.Embedding.injectiveproof · cited by 111
Cited by7
Results whose statement or proof uses this declaration.
- Finsupp.mem_range_mapDomain_iffproof · cited by 1
- MvPolynomial.coeff_killComplproof · cited by 1
- MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subsetproof · cited by 1
- groupHomology.H1CoresCoinfOfTrivial_exactproof · cited by 1
- Finsupp.mapDomain_comapDomain_nat_add_oneproof · cited by 0
- AddMonoidAlgebra.mapDomain_comapDomainproof · cited by 0
- MonoidAlgebra.mapDomain_comapDomainproof · cited by 0