Commit 2025-02-07 20:57 7711b91f

View on Github →

feat(Mathlib/Algebra/Azumaya/Basic): More on azumaya (#21446) I prove that tensor product of Azumaya algebra is still Azumaya, this PR is a prerequisite.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Azumaya/Basic.lean

added theorem IsAzumaya.AlgHom.mulLeftRight_bij

added theorem IsAzumaya.coe_tensorEquivEnd:

added theorem IsAzumaya.mulLeftRight_comp_congr

added theorem IsAzumaya.of_AlgEquiv

Created Mathlib/Algebra/Azumaya/Matrix.lean

added theorem AlgHom.mulLeftRightMatrix.comp_inv:

added theorem AlgHom.mulLeftRightMatrix.inv_comp:

added theorem IsAzumaya.matrix

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

added theorem FaithfulSMul.of_injective

Modified Mathlib/LinearAlgebra/Finsupp/Defs.lean

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean