Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `tensorEquivEnd`	1
Theorems `instIsAzumaya`, `mulLeftRight_bij`, `coe_tensorEquivEnd`, `id`, `mulLeftRight_comp_congr`, `of_AlgEquiv`	6
Total	7

Algebra.IsCentral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsAzumaya` 📖	mathematical	—	`Algebra.IsCentral`	—	`of_algEquiv` `smulCommClass_self` `IsScalarTower.left` `instEnd` `self` `IsAzumaya.bij` `left_of_tensor` `FaithfulSMul.algebraMap_injective` `instFaithfulSMulMulOpposite_1` `IsAzumaya.toFaithfulSMul` `Module.Flat.of_free`

IsAzumaya

Definitions

Name	Category	Theorems
`tensorEquivEnd` 📖	CompOp	1 math math: `coe_tensorEquivEnd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_tensorEquivEnd` 📖	mathematical	—	`AlgHomClass.toAlgHom` `TensorProduct` `MulOpposite` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MulOpposite.instAddCommMonoid` `Algebra.toModule` `Algebra.id` `MulOpposite.instModule` `Module.End` `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` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgEquiv` `Semiring.toModule` `Algebra.to_smulCommClass` `IsScalarTower.right` `AlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `tensorEquivEnd` `AlgHom.mulLeftRight`	—	`Algebra.TensorProduct.ext` `Algebra.to_smulCommClass` `IsScalarTower.right` `smulCommClass_self` `IsScalarTower.left` `LinearMap.instIsScalarTower` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Algebra.ext_id` `IsScalarTower.to_smulCommClass` `AlgHom.ext` `TensorProduct.isScalarTower_left` `LinearMap.ext_ring` `one_smul` `one_mul` `AlgHom.mulLeftRight_apply` `mul_one`
`id` 📖	mathematical	—	`IsAzumaya` `CommSemiring.toSemiring` `Algebra.id`	—	`Module.Projective.of_free` `Module.Free.self` `instFaithfulSMul` `Module.Finite.self` `smulCommClass_self` `IsScalarTower.left` `Algebra.to_smulCommClass` `IsScalarTower.right` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `coe_tensorEquivEnd` `AlgEquiv.bijective`
`mulLeftRight_comp_congr` 📖	mathematical	—	`AlgHom.comp` `TensorProduct` `MulOpposite` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `MulOpposite.instSemiring` `Algebra.toModule` `MulOpposite.instAlgebra` `MulOpposite.instAddCommMonoid` `MulOpposite.instModule` `CommSemiring.toSemiring` `Module.End` `Algebra.TensorProduct.instSemiring` `Module.End.instSemiring` `Algebra.TensorProduct.leftAlgebra` `IsScalarTower.to_smulCommClass` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Algebra.TensorProduct.instAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommSemiring.toCommMonoid` `CommMonoid.toMonoid` `Algebra.toSMul` `AlgHom.mulLeftRight` `AlgEquiv.toAlgHom` `Algebra.TensorProduct.congr` `DFunLike.coe` `Equiv` `AlgEquiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `AlgEquiv.op` `LinearEquiv.conjAlgEquiv` `AlgEquiv.toLinearEquiv`	—	`Algebra.TensorProduct.ext` `smulCommClass_self` `IsScalarTower.left` `LinearMap.instIsScalarTower` `IsScalarTower.to_smulCommClass` `AlgHom.ext` `LinearMap.ext` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.mulLeftRight_apply` `mul_one` `RingHomInvPair.ids` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquiv.apply_symm_apply` `TensorProduct.isScalarTower_left` `one_mul`
`of_AlgEquiv` 📖	mathematical	—	`IsAzumaya` `Ring.toSemiring`	—	`Module.Projective.of_equiv` `toProjective` `FaithfulSMul.of_injective` `toFaithfulSMul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.injective` `Module.Finite.equiv` `toFinite` `smulCommClass_self` `IsScalarTower.left` `IsScalarTower.to_smulCommClass` `Function.Bijective.of_comp_iff` `AlgEquiv.bijective` `AlgEquiv.coe_algHom` `AlgHom.coe_comp` `mulLeftRight_comp_congr`

IsAzumaya.AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mulLeftRight_bij` 📖	mathematical	—	`Function.Bijective` `TensorProduct` `MulOpposite` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `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`	—	`IsAzumaya.bij`

---

← Back to Index