Theorems · Theorem · group theory
MulEquiv.symm_apply_apply
∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (x : M), e.symm (e x) = xe.symm is a left inverse of e, written as e.symm (e y) = y.
- Defined in
- Mathlib.Algebra.Group.Equiv.Defs
- Cited by
- 17 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.symm_apply_applyproof · cited by 320
- MulEquiv.toEquivproof · cited by 126
Cited by17
Results whose statement or proof uses this declaration.
- IsGaloisGroup.intermediateFieldEquivSubgroup_symm_applyproof · cited by 2
- rootsOfUnityEquivOfPrimitiveRoots_symm_applyproof · cited by 1
- Subgroup.characteristic_iff_comap_leproof · cited by 1
- Subgroup.characteristic_iff_le_comapproof · cited by 1
- MulEquivClass.apply_mem_centerproof · cited by 1
- MulEquiv.self_trans_symmproof · cited by 1
- Subgroup.map_equiv_normalizer_eqproof · cited by 1
- HNNExtension.toSubgroupEquiv_neg_applyproof · cited by 1
- MulEquiv.coe_monoidHom_symm_comp_coe_monoidHomproof · cited by 1
- MulEquiv.prime_iffproof · cited by 1
- Submonoid.log_pow_int_eq_selfproof · cited by 0
- Submonoid.LocalizationMap.symm_comp_ofMulEquivOfLocalizations_applyproof · cited by 0