Theorems · Definition · ring theory
IsAzumaya.tensorEquivEnd
(R : Type u_1) → [inst : CommSemiring R] → TensorProduct R R Rᵐᵒᵖ ≃ₐ[R] Module.End R R
The "canonical" isomorphism between R ⊗ Rᵒᵖ and End R R which is equal
to AlgHom.mulLeftRight R R.
- Defined in
- Mathlib.Algebra.Azumaya.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- TensorProductstatement · cited by 2,545
- AlgEquivstatement · cited by 1,681
- MulOppositestatement and proof · cited by 1,135
- Module.Endstatement · cited by 774
- AlgEquiv.transproof · cited by 108
- Algebra.TensorProduct.lidproof · cited by 10
- AlgEquiv.moduleEndSelfproof · cited by 5
Cited by1
Results whose statement or proof uses this declaration.
- IsAzumaya.coe_tensorEquivEndstatement · cited by 0