@[instance_reducible]

instance HexMatrixMathlib.instAdd {R : Type u} {n m : ℕ} [Add R] : Add (Hex.Matrix R n m)

Equations

• HexMatrixMathlib.instAdd = { add := fun (A B : Hex.Matrix R n m) => { data := A.data + B.data } }

@[instance_reducible]

instance HexMatrixMathlib.instNeg {R : Type u} {n m : ℕ} [Neg R] : Neg (Hex.Matrix R n m)

Equations

• HexMatrixMathlib.instNeg = { neg := fun (A : Hex.Matrix R n m) => { data := -A.data } }

@[instance_reducible]

instance HexMatrixMathlib.instSub {R : Type u} {n m : ℕ} [Sub R] : Sub (Hex.Matrix R n m)

Equations

• HexMatrixMathlib.instSub = { sub := fun (A B : Hex.Matrix R n m) => { data := A.data - B.data } }

@[simp]

theorem HexMatrixMathlib.rows_add {R : Type u} {n m : ℕ} [Add R] (A B : Hex.Matrix R n m) : (A + B).rows = A.rows + B.rows

@[simp]

theorem HexMatrixMathlib.rows_neg {R : Type u} {n m : ℕ} [Neg R] (A : Hex.Matrix R n m) : (-A).rows = -A.rows

@[simp]

theorem HexMatrixMathlib.rows_sub {R : Type u} {n m : ℕ} [Sub R] (A B : Hex.Matrix R n m) : (A - B).rows = A.rows - B.rows

@[simp]

theorem HexMatrixMathlib.matrixEquiv_zero {R : Type u} {n m : ℕ} [Zero R] : matrixEquiv 0 = 0

@[simp]

theorem HexMatrixMathlib.matrixEquiv_add {R : Type u} {n m : ℕ} [Add R] (A B : Hex.Matrix R n m) : matrixEquiv (A + B) = matrixEquiv A + matrixEquiv B

@[simp]

theorem HexMatrixMathlib.matrixEquiv_neg {R : Type u} {n m : ℕ} [Neg R] (A : Hex.Matrix R n m) : matrixEquiv (-A) = -matrixEquiv A

@[simp]

theorem HexMatrixMathlib.matrixEquiv_sub {R : Type u} {n m : ℕ} [Sub R] (A B : Hex.Matrix R n m) : matrixEquiv (A - B) = matrixEquiv A - matrixEquiv B

@[simp]

theorem HexMatrixMathlib.matrixEquiv_smul {R : Type u} {n m : ℕ} {S : Type u_1} [SMul S R] (c : S) (A : Hex.Matrix R n m) : matrixEquiv (c • A) = c • matrixEquiv A

@[instance_reducible]

instance HexMatrixMathlib.instOne {R : Type u} {n : ℕ} [OfNat R 0] [OfNat R 1] : One (Hex.Matrix R n n)

1 on a square matrix is the identity matrix. The instance is here rather than in HexMatrix because the Semiring/Ring structures transported below need it, while HexMatrix states its own lemmas with Matrix.identity.

Equations

• HexMatrixMathlib.instOne = { one := Hex.Matrix.identity n }

@[instance_reducible]

instance HexMatrixMathlib.instAddCommMonoid {R : Type u} {n m : ℕ} [AddCommMonoid R] : AddCommMonoid (Hex.Matrix R n m)

Equations

• HexMatrixMathlib.instAddCommMonoid = Function.Injective.addCommMonoid ⇑HexMatrixMathlib.matrixEquiv ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance HexMatrixMathlib.instAddCommGroup {R : Type u} {n m : ℕ} [AddCommGroup R] : AddCommGroup (Hex.Matrix R n m)

Equations

• HexMatrixMathlib.instAddCommGroup = Function.Injective.addCommGroup ⇑HexMatrixMathlib.matrixEquiv ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def HexMatrixMathlib.matrixAddEquiv {R : Type u} {n m : ℕ} [AddCommMonoid R] : Hex.Matrix R n m ≃+ Matrix (Fin n) (Fin m) R

matrixEquiv as an additive equivalence.

Equations

• HexMatrixMathlib.matrixAddEquiv = { toEquiv := HexMatrixMathlib.matrixEquiv, map_add' := ⋯ }

@[simp]

theorem HexMatrixMathlib.matrixAddEquiv_apply {R : Type u} {n m : ℕ} [AddCommMonoid R] (M : Hex.Matrix R n m) : matrixAddEquiv M = matrixEquiv M

@[instance_reducible]

instance HexMatrixMathlib.instModule {R : Type u} {n m : ℕ} [Semiring R] : Module R (Hex.Matrix R n m)

Equations

• HexMatrixMathlib.instModule = Function.Injective.module R HexMatrixMathlib.matrixAddEquiv.toAddMonoidHom ⋯ ⋯

def HexMatrixMathlib.matrixLinearEquiv {R : Type u} {n m : ℕ} [Semiring R] : Hex.Matrix R n m ≃ₗ[R] Matrix (Fin n) (Fin m) R

matrixEquiv as an R-linear equivalence.

Equations

• HexMatrixMathlib.matrixLinearEquiv = { toFun := HexMatrixMathlib.matrixEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := HexMatrixMathlib.matrixEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem HexMatrixMathlib.matrixLinearEquiv_apply {R : Type u} {n m : ℕ} [Semiring R] (M : Hex.Matrix R n m) : matrixLinearEquiv M = matrixEquiv M

@[simp]

theorem HexMatrixMathlib.matrixEquiv_one {R : Type u} {n : ℕ} [Zero R] [One R] : matrixEquiv 1 = 1

@[simp]

theorem HexMatrixMathlib.matrixEquiv_mul {R : Type u} {n : ℕ} [Semiring R] (A B : Hex.Matrix R n n) : matrixEquiv (A * B) = matrixEquiv A * matrixEquiv B

@[instance_reducible]

instance HexMatrixMathlib.instNatCast {R : Type u} {n : ℕ} [Semiring R] : NatCast (Hex.Matrix R n n)

Equations

• HexMatrixMathlib.instNatCast = { natCast := fun (k : ℕ) => HexMatrixMathlib.matrixEquiv.symm ↑k }

@[instance_reducible]

instance HexMatrixMathlib.instIntCast {R : Type u} {n : ℕ} [Ring R] : IntCast (Hex.Matrix R n n)

Equations

• HexMatrixMathlib.instIntCast = { intCast := fun (k : ℤ) => HexMatrixMathlib.matrixEquiv.symm ↑k }

@[instance_reducible]

instance HexMatrixMathlib.instPow {R : Type u} {n : ℕ} [Semiring R] : Pow (Hex.Matrix R n n) ℕ

Equations

• HexMatrixMathlib.instPow = { pow := fun (M : Hex.Matrix R n n) (k : ℕ) => HexMatrixMathlib.matrixEquiv.symm (HexMatrixMathlib.matrixEquiv M ^ k) }

@[simp]

theorem HexMatrixMathlib.matrixEquiv_natCast {R : Type u} {n : ℕ} [Semiring R] (k : ℕ) : matrixEquiv ↑k = ↑k

@[simp]

theorem HexMatrixMathlib.matrixEquiv_intCast {R : Type u} {n : ℕ} [Ring R] (k : ℤ) : matrixEquiv ↑k = ↑k

@[simp]

theorem HexMatrixMathlib.matrixEquiv_pow {R : Type u} {n : ℕ} [Semiring R] (M : Hex.Matrix R n n) (k : ℕ) : matrixEquiv (M ^ k) = matrixEquiv M ^ k

@[instance_reducible]

instance HexMatrixMathlib.instSemiring {R : Type u} {n : ℕ} [Semiring R] : Semiring (Hex.Matrix R n n)

Equations

• HexMatrixMathlib.instSemiring = Function.Injective.semiring ⇑HexMatrixMathlib.matrixEquiv ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance HexMatrixMathlib.instRing {R : Type u} {n : ℕ} [Ring R] : Ring (Hex.Matrix R n n)

Equations

• HexMatrixMathlib.instRing = Function.Injective.ring ⇑HexMatrixMathlib.matrixEquiv ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def HexMatrixMathlib.matrixRingEquiv {R : Type u} {n : ℕ} [Semiring R] : Hex.Matrix R n n ≃+* Matrix (Fin n) (Fin n) R

matrixEquiv as a ring equivalence on square matrices.

Equations

• HexMatrixMathlib.matrixRingEquiv = { toEquiv := HexMatrixMathlib.matrixEquiv, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem HexMatrixMathlib.matrixRingEquiv_apply {R : Type u} {n : ℕ} [Semiring R] (M : Hex.Matrix R n n) : matrixRingEquiv M = matrixEquiv M

@[instance_reducible]

instance HexMatrixMathlib.instAlgebra {R : Type u} {n : ℕ} [CommSemiring R] : Algebra R (Hex.Matrix R n n)

Equations

• HexMatrixMathlib.instAlgebra = Algebra.ofModule ⋯ ⋯

def HexMatrixMathlib.matrixAlgEquiv {R : Type u} {n : ℕ} [CommSemiring R] : Hex.Matrix R n n ≃ₐ[R] Matrix (Fin n) (Fin n) R

matrixEquiv as an R-algebra equivalence on square matrices.

Equations

• HexMatrixMathlib.matrixAlgEquiv = { toEquiv := HexMatrixMathlib.matrixRingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem HexMatrixMathlib.matrixAlgEquiv_apply {R : Type u} {n : ℕ} [CommSemiring R] (M : Hex.Matrix R n n) : matrixAlgEquiv M = matrixEquiv M