Matrix

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

Statistics

Metric	Count
Definitions mulLeftRightMatrix_inv	1
Theorems comp_inv, inv_comp	2
Total	3

AlgHom

Definitions

Name	Category	Theorems
mulLeftRightMatrix_inv 📖	CompOp	2 math math: mulLeftRightMatrix.inv_comp, mulLeftRightMatrix.comp_inv

AlgHom.mulLeftRightMatrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_inv 📖	mathematical	—	LinearMap.comp Module.End Matrix CommSemiring.toSemiring Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Matrix.module Semiring.toModule TensorProduct MulOpposite Matrix.semiring MulOpposite.instAddCommMonoid Algebra.toModule Matrix.instAlgebra Algebra.id MulOpposite.instModule LinearMap.addCommMonoid RingHom.id Algebra.TensorProduct.instSemiring MulOpposite.instSemiring MulOpposite.instAlgebra Module.End.instSemiring LinearMap.module Matrix.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.TensorProduct.instAlgebra Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid Algebra.toSMul IsScalarTower.left RingHomCompTriple.ids AlgHom.toLinearMap AlgHom.mulLeftRight AlgHom.mulLeftRightMatrix_inv LinearMap.id	—	LinearMap.ext Matrix.smulCommClass Algebra.to_smulCommClass smulCommClass_self IsScalarTower.left RingHomCompTriple.ids Module.Basis.ext Finite.of_fintype Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass Matrix.stdBasis_eq_single LinearMap.coe_sum Finset.sum_apply Matrix.ext ite_and AlgHom.mulLeftRight_apply Matrix.sum_apply mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq Fintype.sum_prod_type Finset.sum_ite_eq' Finset.sum_ite_irrel Finset.sum_const_zero
inv_comp 📖	mathematical	—	LinearMap.comp TensorProduct Matrix MulOpposite NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Matrix.semiring CommSemiring.toSemiring MulOpposite.instAddCommMonoid Algebra.toModule Matrix.instAlgebra Algebra.id MulOpposite.instModule Module.End Matrix.addCommMonoid Matrix.module Semiring.toModule Algebra.TensorProduct.instSemiring MulOpposite.instSemiring MulOpposite.instAlgebra LinearMap.addCommMonoid RingHom.id TensorProduct.addCommMonoid Algebra.TensorProduct.instAlgebra LinearMap.module Matrix.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass TensorProduct.instModule RingHomCompTriple.ids AlgHom.mulLeftRightMatrix_inv AlgHom.toLinearMap Module.End.instSemiring Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid Algebra.toSMul IsScalarTower.left AlgHom.mulLeftRight LinearMap.id	—	Module.Basis.ext IsScalarTower.to_smulCommClass Matrix.isScalarTower IsScalarTower.right Finite.of_fintype Matrix.smulCommClass Algebra.to_smulCommClass RingHomCompTriple.ids smulCommClass_self IsScalarTower.left Module.Basis.tensorProduct_apply Matrix.stdBasis_eq_single ite_and RingHomInvPair.ids Finset.sum_congr Fintype.sum_prod_type AlgHom.mulLeftRight_apply mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq ite_smul one_smul zero_smul Finset.sum_ite_eq' Finset.sum_ite_irrel Finset.sum_const_zero

---

← Back to Index