Theorems · Theorem · group theory
MulEquiv.apply_symm_apply
∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (y : N), e (e.symm y) = ye.symm is a right inverse of e, written as e (e.symm y) = y.
- 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.
Cites5
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
- MulEquiv.symmstatement · cited by 482
- Equiv.apply_symm_applyproof · cited by 346
- MulEquiv.toEquivproof · cited by 126
Cited by37
Results whose statement or proof uses this declaration.
- MonoidHom.apply_ofInjective_symmproof · cited by 4
- IsGaloisGroup.of_mulEquivproof · cited by 4
- IsGaloisGroup.mulEquivCongr_apply_smulproof · cited by 3
- MulEquiv.uniqueFactorizationMonoidproof · cited by 3
- Submonoid.mul_leftInvEquiv_symmproof · cited by 2
- MulChar.domRestrictHom_surjectiveproof · cited by 1
- HNNExtension.of_mul_tproof · cited by 1
- Ideal.stabilizerEquiv_symm_apply_smulproof · cited by 1
- autEquivRootsOfUnity_apply_rootOfSplitproof · cited by 1
- MulEquiv.strictMono_symmproof · cited by 1
- HNNExtension.toSubgroupEquiv_neg_applyproof · cited by 1