Theorems · Theorem · general algebraic systems
Finsupp.mapDomain_injective
∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β},
Function.Injective f → Function.Injective (Finsupp.mapDomain f)- Defined in
- Mathlib.Data.Finsupp.Basic
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 73 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.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- AddCommMonoidstatement and proof · cited by 12,281
- Finsuppstatement and proof · cited by 5,255
- Finsupp.extproof · cited by 399
- Finsupp.mapDomainstatement and proof · cited by 168
- Finsupp.mapDomain_applyproof · cited by 11
Cited by16
Results whose statement or proof uses this declaration.
- LinearIndependent.compproof · cited by 41
- MvPolynomial.rename_injectiveproof · cited by 11
- MvPolynomial.coeff_rename_mapDomainproof · cited by 6
- MvPolynomial.support_rename_of_injectiveproof · cited by 3
- Module.length_finsuppproof · cited by 2
- MvPolynomial.coeff_killComplproof · cited by 1
- Matrix.PosDef.submatrixproof · cited by 1
- AddMonoidAlgebra.mapDomain_injectiveproof · cited by 1
- Algebra.Generators.cotangentRestrict_bijective_of_isComplproof · cited by 1
- MvPolynomial.support_killComplstatement · cited by 1
- MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_leproof · cited by 1
- Finsupp.lcomapDomain_eq_linearProjOfIsComplstatement and proof · cited by 1