Theorems · Theorem · group theory
AddEquiv.surjective
∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N), Function.Surjective ⇑e- Defined in
- Mathlib.Algebra.Group.Equiv.Defs
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- AddEquivstatement and proof · cited by 1,087
- EquivLike.surjectiveproof · cited by 24
Cited by37
Results whose statement or proof uses this declaration.
- AddEquiv.isAddCyclicproof · cited by 4
- AddAction.IsBlock.translateproof · cited by 4
- AddEquiv.isWeaklyRegular_congrproof · cited by 3
- Algebra.Generators.map_toComp_kerproof · cited by 3
- Function.Exact.iff_of_ladder_addEquivproof · cited by 3
- AddChar.card_eqproof · cited by 2
- CochainComplex.HomComplex.Cochain.toSingleMk_surjectiveproof · cited by 2
- CochainComplex.HomComplex.Cochain.fromSingleMk_surjectiveproof · cited by 2
- CochainComplex.HomComplex.Cochain.δ_rightUnshiftproof · cited by 2
- AddEquiv.range_eq_topproof · cited by 1
- AddGroup.rank_congrproof · cited by 1
- AddAction.isPreprimitive_fixingAddSubgroup_insert_iffproof · cited by 1