Theorems · Definition · group theory
MonoidHom.ofInjective
{G : Type u_1} →
[inst : Group G] → {N : Type u_5} → [inst_1 : Group N] → {f : G →* N} → Function.Injective ⇑f → G ≃* ↥f.rangeThe range of an injective group homomorphism is isomorphic to its domain.
- Defined in
- Mathlib.Algebra.Group.Subgroup.Ker
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Groupstatement and proof · cited by 6,238
- MonoidHomstatement and proof · cited by 3,629
- Subgroupstatement · cited by 3,593
- MulEquivstatement · cited by 1,142
- MonoidHom.rangestatement and proof · cited by 314
- MonoidHom.codRestrictproof · cited by 8
- MulEquiv.ofBijectiveproof · cited by 5
Cited by16
Results whose statement or proof uses this declaration.
- Monoid.PushoutI.NormalWord.consproof · cited by 7
- MonoidHom.apply_ofInjective_symmstatement and proof · cited by 4
- Monoid.PushoutI.NormalWord.rconsproof · cited by 3
- Monoid.PushoutI.NormalWord.prod_consproof · cited by 2
- isCyclic_of_injectiveproof · cited by 2
- Monoid.PushoutI.NormalWord.cons_eq_smulproof · cited by 1
- GroupExtension.conjActproof · cited by 1
- Group.isCyclic_of_coprime_card_range_card_kerproof · cited by 1
- Monoid.PushoutI.NormalWord.prod_summand_smulproof · cited by 1
- Polynomial.Gal.galActionHom_bijective_of_prime_degreeproof · cited by 1
- Monoid.PushoutI.NormalWord.cons_headstatement · cited by 0
- Sylow.mulEquivIteratedWreathProductproof · cited by 0