Theorems · Theorem · group theory
AddMonoidHom.range_eq_map
∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N), f.range = AddSubgroup.map f ⊤- Defined in
- Mathlib.Algebra.Group.Subgroup.Ker
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Top.topstatement · cited by 9,680
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement · cited by 3,232
- AddMonoidHomstatement and proof · cited by 3,230
- AddSubgroup.mapstatement · cited by 189
- AddMonoidHom.rangestatement · cited by 142
- AddSubgroup.extproof · cited by 75
- AddSubgroup.mem_topproof · cited by 29
- AddMonoidHom.mem_rangeproof · cited by 16
- AddSubgroup.mem_mapproof · cited by 15
Cited by15
Results whose statement or proof uses this declaration.
- AddMonoidHom.map_rangeproof · cited by 5
- AddSubgroup.top_subtype_lowerCentralSeriesproof · cited by 4
- AddSubgroup.isAddCyclic_iff_exists_zmultiples_eq_topproof · cited by 4
- AddSubgroup.Normal.mapproof · cited by 3
- AddSubgroup.map_le_rangeproof · cited by 2
- AddGroup.nilpotent_of_surjectiveproof · cited by 2
- AddSubgroup.map_subtype_addCommutatorproof · cited by 2
- AddSubgroup.IsSubnormal.trans'proof · cited by 2
- AddGroup.nilpotencyClass_le_of_surjectiveproof · cited by 1
- AddMonoid.Coprod.range_eqproof · cited by 1
- AddEquiv.map_range_nsmulAddMonoidHomproof · cited by 1
- AddMonoidHom.range_eq_bot_iffproof · cited by 1