Action

📁 Source: Mathlib/Data/Matrix/Action.lean

Statistics

Metric	Count
Definitions instModuleForall, instModuleMulOppositeForall	2
Theorems instIsScalarTowerForall, instIsScalarTowerMulOppositeForallOfSMulCommClass, instSMulCommClassForall, instSMulCommClassForall_1, instSMulCommClassMulOppositeForallOfIsScalarTower, instSMulCommClassMulOppositeForallOfIsScalarTower_1, op_smul_eq_vecMul, smul_eq_mulVec	8
Total	10

Matrix

Definitions

Name	Category	Theorems
instModuleForall 📖	CompOp	4 math math: instSMulCommClassForall_1, instIsScalarTowerForall, smul_eq_mulVec, instSMulCommClassForall
instModuleMulOppositeForall 📖	CompOp	4 math math: instSMulCommClassMulOppositeForallOfIsScalarTower_1, instSMulCommClassMulOppositeForallOfIsScalarTower, instIsScalarTowerMulOppositeForallOfSMulCommClass, op_smul_eq_vecMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsScalarTowerForall 📖	mathematical	—	IsScalarTower Matrix smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass Pi.addZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Pi.addMonoid Module.toDistribMulAction Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModuleForall Function.hasSMul	—	smul_mulVec
instIsScalarTowerMulOppositeForallOfSMulCommClass 📖	mathematical	—	IsScalarTower MulOpposite Matrix MulOpposite.instSMul smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass Pi.addZeroClass DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Pi.addMonoid Module.toDistribMulAction MulOpposite.instSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModuleMulOppositeForall Function.hasSMul	—	vecMul_smul
instSMulCommClassForall 📖	mathematical	—	SMulCommClass Matrix SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Pi.addMonoid Module.toDistribMulAction Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModuleForall Function.hasSMul	—	mulVec_smul SMulCommClass.symm
instSMulCommClassForall_1 📖	mathematical	—	SMulCommClass Matrix Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass Pi.addZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Pi.addMonoid Module.toDistribMulAction Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModuleForall	—	mulVec_smul
instSMulCommClassMulOppositeForallOfIsScalarTower 📖	mathematical	—	SMulCommClass MulOpposite Matrix SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Pi.addMonoid Module.toDistribMulAction MulOpposite.instSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModuleMulOppositeForall Function.hasSMul	—	smul_vecMul
instSMulCommClassMulOppositeForallOfIsScalarTower_1 📖	mathematical	—	SMulCommClass MulOpposite Matrix Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass Pi.addZeroClass DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Pi.addMonoid Module.toDistribMulAction MulOpposite.instSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModuleMulOppositeForall	—	smul_vecMul
op_smul_eq_vecMul 📖	mathematical	—	MulOpposite Matrix SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulOpposite.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Pi.addMonoid Module.toDistribMulAction MulOpposite.instSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModuleMulOppositeForall vecMul MulOpposite.unop	—	—
smul_eq_mulVec 📖	mathematical	—	Matrix SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero Pi.addZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring Pi.addMonoid Module.toDistribMulAction Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring instModuleForall mulVec	—	—

---

← Back to Index