Theorems · Theorem
Equiv.apply_symm_apply
∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : β), e (e.symm x) = x- Defined in
- Mathlib.Logic.Equiv.Defs
- Cited by
- 346 results in Mathlib
- Foundations
- Depth 14 from the axioms, rests on 58 definitions · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Equivstatement and proof · cited by 8,337
- Equiv.symmstatement · cited by 3,681
- Equiv.right_invproof · cited by 68
Cited by348
Results whose statement or proof uses this declaration.
- AlgEquiv.apply_symm_applyproof · cited by 67
- RingEquiv.apply_symm_applyproof · cited by 53
- Matrix.det_mulproof · cited by 51
- OrderIso.apply_symm_applyproof · cited by 45
- MulEquiv.apply_symm_applyproof · cited by 37
- AddEquiv.apply_symm_applyproof · cited by 37
- Equiv.forall_congr_rightproof · cited by 28
- Equiv.self_comp_symmproof · cited by 28
- Equiv.forall_congrproof · cited by 22
- Homeomorph.apply_symm_applyproof · cited by 18
- DirectSum.decompose_coeproof · cited by 17
- Finsupp.mapDomain_equiv_applyproof · cited by 15
Showing the 200 most cited of 348.