Theorems · Theorem · group theory
AddEquiv.symm_apply_eq
∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) {x : N} {y : M}, e.symm x = y ↔ x = e y- Defined in
- Mathlib.Algebra.Group.Equiv.Defs
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, 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
- AddEquiv.toEquivproof · cited by 174
- Equiv.symm_apply_eqproof · cited by 63
Cited by8
Results whose statement or proof uses this declaration.
- DFinsupp.comp_liftAddHomproof · cited by 4
- zmodAddEquivOfGenerator_symm_apply_zsmulproof · cited by 2
- lift_rank_eq_of_equiv_equivproof · cited by 2
- Finsupp.toMultiset_eq_iffproof · cited by 0
- AddCon.comapQuotientEquivOfSurj_symm_mkproof · cited by 0
- AddCon.comapQuotientEquivOfSurj_symm_mk'proof · cited by 0
- Finsupp.comp_liftAddHomproof · cited by 0
- MonomialOrder.toWithBotSyn_symm_apply_eq_botproof · cited by 0