Mathlib algebraic structure on Hex.Matrix, transported along matrixEquiv.

matrixEquiv carries the executable dense-matrix operations to Mathlib's function-based Matrix, so we equip Hex.Matrix with the Mathlib algebraic tower (AddCommMonoid, AddCommGroup, Module, Semiring, Ring, Algebra) whose operations are the executable ones, and upgrade matrixEquiv to the corresponding additive, linear, ring, and algebra equivalences.

Base operations on the opaque structure

The abbreviation representation inherited these pointwise operations from Vector; the opaque structure delegates them to the row data, so the Mathlib tower transported along matrixEquiv has executable operations.

@[implicit_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 } }

@[implicit_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 } }

@[implicit_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

Preservation of the additive operations

@[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

@[implicit_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 }

Additive instances and the additive equivalence

@[implicit_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 ⋯ ⋯ ⋯ ⋯

@[implicit_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

Module structure and the linear equivalence

@[implicit_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

Multiplicative preservation

@[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

Auxiliary operations, pulled back through matrixEquiv

These NatCast, IntCast, and Pow instances exist only to populate the corresponding fields of the Semiring/Ring structures. They are proof-facing: defined by transport through matrixEquiv, not in executable form. Executable code never goes through them — it uses the HexMatrix operations directly (the square-matrix *, the ofFn identity). Their transport lemmas below reduce them to the Mathlib side for simp/grind.

@[implicit_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 }

@[implicit_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 }

@[implicit_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

Ring structure and the ring equivalence

@[implicit_reducible]

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

Equations

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

@[implicit_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

Algebra structure and the algebra equivalence

@[implicit_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