mulLeftRight_bij — Mathlib

English

If A is Azumaya over R, then the canonical multiplication-left-right map AlgHom.mulLeftRight R A is bijective onto End_R(A).

Русский

Если A является Azumaya над R, то каноническое отображение AlgHom.mulLeftRight R A является биективным на End_R(A).

LaTeX

$$$\text{mulLeftRight}: A \otimes_R A^{op} \to \mathrm{End}_R(A) \text{ is bijective when } A \text{ is Azumaya over } R$$$

Lean4

theorem mulLeftRight_bij [h : IsAzumaya R A] : Function.Bijective (AlgHom.mulLeftRight R A) :=
  h.bij

Похожие утверждения