Theorems · Definition · group theory
MulEquiv.ofBijective
{M : Type u_9} →
{N : Type u_10} →
{F : Type u_11} →
[inst : Mul M] →
[inst_1 : Mul N] → [inst_2 : FunLike F M N] → [MulHomClass F M N] → (f : F) → Function.Bijective ⇑f → M ≃* NA bijective Semigroup homomorphism is an isomorphism
- Defined in
- Mathlib.Algebra.Group.Equiv.Defs
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses Classical.choice
- Assumes
- MulMulFunLikeMulHomClass
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
- Equivproof · cited by 8,337
- FunLikestatement and proof · cited by 2,560
- MulEquivstatement · cited by 1,142
- map_mulproof · cited by 1,137
- Function.Bijectivestatement and proof · cited by 863
- MulHomClassstatement and proof · cited by 73
- Equiv.ofBijectiveproof · cited by 70
Cited by21
Results whose statement or proof uses this declaration.
- powMulEquivproof · cited by 12
- MonoidHom.ofInjectiveproof · cited by 12
- intEquivOfZPowersEqTopproof · cited by 11
- IsGaloisGroup.mulEquivAlgEquivproof · cited by 10
- QuotientGroup.quotientKerEquivRangeproof · cited by 7
- SemidirectProduct.mulEquivSubgroupproof · cited by 3
- MulEquiv.ofBijective_applystatement and proof · cited by 2
- QuotientGroup.liftEquivproof · cited by 2
- CategoryTheory.PreGaloisCategory.toAutMulEquivproof · cited by 2
- StarMulEquiv.ofBijectiveproof · cited by 2
- Sylow.directProductOfNormalproof · cited by 1
- Matrix.ProjectiveSpecialLinearGroup.isoPSLOfAlgClosedproof · cited by 0