Theorems · Definition · ring theory

AlgHom.mulLeftRight

(R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → TensorProduct R A Aᵐᵒᵖ →ₐ[R] Module.End R A

The canonical map from A ⊗[R] Aᵐᵒᵖ to Module.End R A where a ⊗ b maps to f : x ↦ a * x * b.

Defined in

Mathlib.Algebra.Azumaya.Defs

Cited by

8 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebra