Actions by matrices on vectors through *ᵥ and ᵥ*, cast as Modules

This file provides the left- and right- module structures of square matrices on vectors, via Matrix.mulVec and Matrix.vecMul.

*ᵥ as a left-module

@[instance_reducible]

instance Matrix.instModuleForall {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] : Module (Matrix n n R) (n → R)

Equations

• Matrix.instModuleForall = { smul := Matrix.mulVec, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[simp]

theorem Matrix.smul_eq_mulVec {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] (A : Matrix n n R) (v : n → R) : A • v = A.mulVec v

instance Matrix.instSMulCommClassForall {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [DistribSMul S R] [SMulCommClass R S R] : SMulCommClass (Matrix n n R) S (n → R)

instance Matrix.instSMulCommClassForall_1 {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [DistribSMul S R] [SMulCommClass S R R] : SMulCommClass S (Matrix n n R) (n → R)

instance Matrix.instIsScalarTowerForall {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [DistribSMul S R] [IsScalarTower S R R] : IsScalarTower S (Matrix n n R) (n → R)

theorem Matrix.ext_iff_smul {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] {A B : Matrix n n R} : A = B ↔ ∀ (v : n → R), A • v = B • v

*ᵥ as a right-module

@[instance_reducible]

instance Matrix.instModuleMulOppositeForall {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] : Module (Matrix n n R)ᵐᵒᵖ (n → R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.op_smul_eq_vecMul {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] (A : (Matrix n n R)ᵐᵒᵖ) (v : n → R) : A • v = vecMul v (MulOpposite.unop A)

instance Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [DistribSMul S R] [IsScalarTower S R R] : SMulCommClass (Matrix n n R)ᵐᵒᵖ S (n → R)

instance Matrix.instSMulCommClassMulOppositeForallOfIsScalarTower_1 {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [DistribSMul S R] [IsScalarTower S R R] : SMulCommClass S (Matrix n n R)ᵐᵒᵖ (n → R)

instance Matrix.instIsScalarTowerMulOppositeForallOfSMulCommClass {n : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype n] [DecidableEq n] [Semiring R] [DistribSMul S R] [SMulCommClass S R R] : IsScalarTower S (Matrix n n R)ᵐᵒᵖ (n → R)