Theorems · Theorem · general algebraic systems
Finsupp.mapRange_injective
∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (e : M → N) (he₀ : e 0 = 0),
Function.Injective e → Function.Injective (Finsupp.mapRange e he₀)Finsupp.mapRange of an injective function is injective.
- Defined in
- Mathlib.Data.Finsupp.Defs
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
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.mapRangestatement and proof · cited by 91
- Finsupp.ext_iffproof · cited by 10
Cited by7
Results whose statement or proof uses this declaration.
- Finsupp.mapRange_bijectiveproof · cited by 1
- linearIndependent_smulproof · cited by 0
- groupHomology.single_isCycle₂_iffproof · cited by 0
- MonoidAlgebra.map_injectiveproof · cited by 0
- groupHomology.chainsMap_f_map_monoproof · cited by 0
- groupHomology.single_mem_cycles₂_iffproof · cited by 0
- AddMonoidAlgebra.map_injectiveproof · cited by 0