Theorems · Theorem · group theory
MulEquiv.injective
∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), Function.Injective ⇑e- Defined in
- Mathlib.Algebra.Group.Equiv.Defs
- Cited by
- 36 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
- MulEquivstatement and proof · cited by 1,142
- EquivLike.injectiveproof · cited by 32
Cited by36
Results whose statement or proof uses this declaration.
- MulEquiv.isFieldproof · cited by 14
- MulEquiv.isDomainproof · cited by 8
- ClassGroup.mk_eq_one_iffproof · cited by 4
- Monoid.exponent_eq_of_mulEquivproof · cited by 4
- IsGaloisGroup.of_mulEquivproof · cited by 4
- Sylow.normalizer_sup_eq_topproof · cited by 2
- MulEquivClass.map_nonZeroDivisorsproof · cited by 2
- Function.MulExact.iff_of_ladder_mulEquivproof · cited by 2
- gal_isSolvable_towerproof · cited by 1
- MulEquivClass.apply_mem_centerproof · cited by 1
- MulEquivClass.isDedekindFiniteMonoid_iffproof · cited by 1