Theorems · Definition · ring theory

AlgHom.mulLeftRightMatrix_inv

(R : Type u_1) →
  (n : Type u_2) →
    [inst : CommSemiring R] →
      [Fintype n] → [DecidableEq n] → Module.End R (Matrix n n R) →ₗ[R] TensorProduct R (Matrix n n R) (Matrix n n R)ᵐᵒᵖ

AlgHom.mulLeftRight for matrix algebra sends basis Eᵢⱼ⊗Eₖₗ to the map f : Eₛₜ ↦ Eᵢⱼ * Eₛₜ * Eₖₗ = δⱼₛδₜₖEᵢₗ, therefore we construct the inverse by sending f to ∑ᵢₗₛₜ f(Eₛₜ)ᵢₗ • Eᵢₛ⊗Eₜₗ.

Defined in

Mathlib.Algebra.Azumaya.Matrix

Cited by

3 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringFintypeDecidableEq