Documentation Verification Report

Defs

📁 Source: Mathlib/Algebra/Azumaya/Defs.lean

Statistics

Metric	Count
Definitions `mulLeftRight`, `IsAzumaya`, `instModuleTensorProductMop`	3
Theorems `mulLeftRight_apply`, `bij`, `toFaithfulSMul`, `toFinite`, `toProjective`	5
Total	8

AlgHom

Definitions

Name	Category	Theorems
`mulLeftRight` 📖	CompOp	7 math math: `mulLeftRightMatrix.inv_comp`, `IsAzumaya.mulLeftRight_comp_congr`, `mulLeftRight_apply`, `IsAzumaya.bij`, `IsAzumaya.coe_tensorEquivEnd`, `mulLeftRightMatrix.comp_inv`, `IsAzumaya.AlgHom.mulLeftRight_bij`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeftRight_apply` 📖	mathematical	—	`DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `RingHom.id` `AlgHom` `TensorProduct` `MulOpposite` `MulOpposite.instAddCommMonoid` `MulOpposite.instModule` `Algebra.TensorProduct.instSemiring` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Module.End.instSemiring` `Algebra.TensorProduct.instAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `funLike` `mulLeftRight` `TensorProduct.tmul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `MulOpposite.unop`	—	`smulCommClass_self` `IsScalarTower.left` `IsScalarTower.right`

IsAzumaya

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bij` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `MulOpposite` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulOpposite.instAddCommMonoid` `Algebra.toModule` `MulOpposite.instModule` `CommSemiring.toSemiring` `Module.End` `DFunLike.coe` `AlgHom` `Algebra.TensorProduct.instSemiring` `MulOpposite.instSemiring` `MulOpposite.instAlgebra` `Module.End.instSemiring` `Algebra.TensorProduct.instAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `AlgHom.mulLeftRight`	—	—
`toFaithfulSMul` 📖	mathematical	—	`FaithfulSMul` `Algebra.toSMul`	—	—
`toFinite` 📖	mathematical	—	`Module.Finite` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule`	—	—
`toProjective` 📖	mathematical	—	`Module.Projective` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule`	—	—

(root)

Definitions

Name	Category	Theorems
`IsAzumaya` 📖	CompData	3 math math: `IsAzumaya.id`, `IsAzumaya.of_AlgEquiv`, `IsAzumaya.matrix`
`instModuleTensorProductMop` 📖	CompOp	—

---

← Back to Index