Mathlib Map

Structures · Algebra

IsAzumaya

An Azumaya algebra is a finitely generated, projective and faithful R-algebra where AlgHom.mulLeftRight R A : (A ⊗[R] Aᵐᵒᵖ) →ₐ[R] Module.End R A is an isomorphism.

Defined in
Mathlib.Algebra.Azumaya.Defs
Shape
2 explicit arguments · adds bij

Extends3

Extended by0

Nothing extends this class yet.

Concrete types that are instances0

No instance on a concrete type; it is reached through other classes.

How is a type an instance?

Loading the hierarchy index…

Assumed by7

Ancestors3