Theorems · Theorem · general algebraic systems
Finsupp.mapRange_surjective
∀ {α : 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.Surjective e → Function.Surjective (Finsupp.mapRange e he₀)Finsupp.mapRange of a surjective function is surjective.
- Defined in
- Mathlib.Data.Finsupp.Defs
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Setproof · cited by 53,352
- Set.ofPredproof · cited by 6,101
- Finsuppstatement and proof · cited by 5,255
- Set.univproof · cited by 3,945
- Finsupp.mapRangestatement · cited by 91
- Function.Surjective.range_eqproof · cited by 70
- Set.range_eq_univproof · cited by 50
- Finsupp.range_mapRangeproof · cited by 3
Cited by7
Results whose statement or proof uses this declaration.
- Finsupp.mapRange_bijectiveproof · cited by 1
- AddMonoidAlgebra.map_surjectiveproof · cited by 0
- groupHomology.H1CoresCoinf_exactproof · cited by 0
- groupHomology.chainsMap_f_map_epiproof · cited by 0
- Module.free_quotSMulTop_iff_freeproof · cited by 0
- MonoidAlgebra.map_surjectiveproof · cited by 0