Theorems · Definition · ring theory
MulOpposite.opEquiv
{α : Type u_1} → α ≃ αᵐᵒᵖThe canonical bijection between α and αᵐᵒᵖ.
- Defined in
- Mathlib.Algebra.Opposites
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equivstatement · cited by 8,337
- MulOppositestatement · cited by 1,135
- MulOpposite.opproof · cited by 520
- MulOpposite.unopproof · cited by 268
- MulOpposite.op_unopproof · cited by 3
- MulOpposite.unop_opproof · cited by 1
Cited by39
Results whose statement or proof uses this declaration.
- DomMulAct.mkproof · cited by 56
- MulOpposite.opAddEquivproof · cited by 25
- MulOpposite.opHomeomorphproof · cited by 17
- starMulEquivproof · cited by 7
- MulOpposite.opEquiv_applystatement and proof · cited by 7
- MulEquiv.inv'proof · cited by 4
- Subgroup.equivOpproof · cited by 4
- MonoidAlgebra.opRingEquivproof · cited by 4
- MulOpposite.opMulEquivproof · cited by 4
- CategoryTheory.PreGaloisCategory.endMulEquivAutGaloisproof · cited by 3
- MulOpposite.opEquiv_symm_applystatement and proof · cited by 3
- isLeftRegular_opproof · cited by 3