Theorems · Theorem · group theory
AddEquiv.apply_symm_apply
∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add 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
- AddEquivstatement and proof · cited by 1,087
- AddEquiv.symmstatement · cited by 530
- Equiv.apply_symm_applyproof · cited by 346
- AddEquiv.toEquivproof · cited by 174
Cited by37
Results whose statement or proof uses this declaration.
- MonomialOrder.le_degreeproof · cited by 11
- MonomialOrder.degree_add_leproof · cited by 5
- DFinsupp.toMultiset_toDFinsuppproof · cited by 4
- MonomialOrder.degree_le_iffproof · cited by 3
- MonomialOrder.degree_monomial_leproof · cited by 3
- Algebra.Generators.map_toComp_kerproof · cited by 3
- lift_rank_eq_of_equiv_equivproof · cited by 2
- HahnSeries.addOppositeEquiv_symm_orderTopproof · cited by 2
- CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcompproof · cited by 2
- CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precompproof · cited by 2
- AddCommGrpCat.isColimit_iff_bijective_descproof · cited by 1
- MonomialOrder.degree_le_degree_of_support_subsetproof · cited by 1