The convolutive star ring on matrices

In this file, we provide the star algebra instance on WithConv (Matrix m n R) given by the Hadamard product and intrinsic star (i.e., the star of each element in the matrix).

@[instance_reducible]

instance instMulWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [Mul α] : Mul (WithConv (Matrix m n α))

Equations

• instMulWithConvMatrix = { mul := fun (a b : WithConv (Matrix m n α)) => WithConv.toConv (a.ofConv.hadamard b.ofConv) }

theorem convMul_def {α : Type u_1} {m : Type u_3} {n : Type u_4} [Mul α] (x y : WithConv (Matrix m n α)) : x * y = WithConv.toConv (x.ofConv.hadamard y.ofConv)

@[instance_reducible]

instance instSemigroupWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [Semigroup α] : Semigroup (WithConv (Matrix m n α))

Equations

• instSemigroupWithConvMatrix = { toMul := instMulWithConvMatrix, mul_assoc := ⋯ }

@[instance_reducible]

instance instNonUnitalNonAssocSemiringWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring (WithConv (Matrix m n α))

Equations

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

@[instance_reducible]

instance instCommMagmaWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [CommMagma α] : CommMagma (WithConv (Matrix m n α))

Equations

• instCommMagmaWithConvMatrix = { toMul := instMulWithConvMatrix, mul_comm := ⋯ }

@[instance_reducible]

instance instOneWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [One α] : One (WithConv (Matrix m n α))

Equations

• instOneWithConvMatrix = { one := WithConv.toConv (Matrix.of 1) }

theorem convOne_def {α : Type u_1} {m : Type u_3} {n : Type u_4} [One α] : 1 = WithConv.toConv (Matrix.of 1)

@[instance_reducible]

instance instMulOneClassWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [MulOneClass α] : MulOneClass (WithConv (Matrix m n α))

Equations

• instMulOneClassWithConvMatrix = { toOne := instOneWithConvMatrix, toMul := instMulWithConvMatrix, one_mul := ⋯, mul_one := ⋯ }

@[instance_reducible]

instance instMonoidWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [Monoid α] : Monoid (WithConv (Matrix m n α))

Equations

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

@[instance_reducible]

instance instCommMonoidWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [CommMonoid α] : CommMonoid (WithConv (Matrix m n α))

Equations

• instCommMonoidWithConvMatrix = { toMonoid := instMonoidWithConvMatrix, mul_comm := ⋯ }

@[instance_reducible]

instance instNonAssocSemiringWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonAssocSemiring α] : NonAssocSemiring (WithConv (Matrix m n α))

Equations

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

@[instance_reducible]

instance instNonUnitalSemiringWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalSemiring α] : NonUnitalSemiring (WithConv (Matrix m n α))

Equations

• instNonUnitalSemiringWithConvMatrix = { toNonUnitalNonAssocSemiring := instNonUnitalNonAssocSemiringWithConvMatrix, mul_assoc := ⋯ }

@[instance_reducible]

instance instNonUnitalNonAssocCommSemiringWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalNonAssocCommSemiring α] : NonUnitalNonAssocCommSemiring (WithConv (Matrix m n α))

Equations

• instNonUnitalNonAssocCommSemiringWithConvMatrix = { toNonUnitalNonAssocSemiring := instNonUnitalNonAssocSemiringWithConvMatrix, mul_comm := ⋯ }

@[instance_reducible]

instance instNonUnitalCommSemiringWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalCommSemiring α] : NonUnitalCommSemiring (WithConv (Matrix m n α))

Equations

• instNonUnitalCommSemiringWithConvMatrix = { toNonUnitalSemiring := instNonUnitalSemiringWithConvMatrix, mul_comm := ⋯ }

@[instance_reducible]

instance instNonAssocCommSemiringWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonAssocCommSemiring α] : NonAssocCommSemiring (WithConv (Matrix m n α))

Equations

• instNonAssocCommSemiringWithConvMatrix = { toNonAssocSemiring := instNonAssocSemiringWithConvMatrix, mul_comm := ⋯ }

@[instance_reducible]

instance instSemiringWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [Semiring α] : Semiring (WithConv (Matrix m n α))

Equations

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

@[instance_reducible]

instance instCommSemiringWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [CommSemiring α] : CommSemiring (WithConv (Matrix m n α))

Equations

• instCommSemiringWithConvMatrix = { toSemiring := instSemiringWithConvMatrix, mul_comm := ⋯ }

@[instance_reducible]

instance instNonUnitalNonAssocRingWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing (WithConv (Matrix m n α))

Equations

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

@[instance_reducible]

instance instNonUnitalNonAssocCommRingWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalNonAssocCommRing α] : NonUnitalNonAssocCommRing (WithConv (Matrix m n α))

Equations

• instNonUnitalNonAssocCommRingWithConvMatrix = { toNonUnitalNonAssocRing := instNonUnitalNonAssocRingWithConvMatrix, mul_comm := ⋯ }

@[instance_reducible]

instance instNonUnitalRingWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalRing α] : NonUnitalRing (WithConv (Matrix m n α))

Equations

• instNonUnitalRingWithConvMatrix = { toNonUnitalNonAssocRing := instNonUnitalNonAssocRingWithConvMatrix, mul_assoc := ⋯ }

@[instance_reducible]

instance instNonUnitalCommRingWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalCommRing α] : NonUnitalCommRing (WithConv (Matrix m n α))

Equations

• instNonUnitalCommRingWithConvMatrix = { toNonUnitalRing := instNonUnitalRingWithConvMatrix, mul_comm := ⋯ }

@[instance_reducible]

instance instNonAssocRingWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonAssocRing α] : NonAssocRing (WithConv (Matrix m n α))

Equations

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

@[instance_reducible]

instance instNonAssocCommRingWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonAssocCommRing α] : NonAssocCommRing (WithConv (Matrix m n α))

Equations

• instNonAssocCommRingWithConvMatrix = { toNonAssocRing := instNonAssocRingWithConvMatrix, mul_comm := ⋯ }

@[instance_reducible]

instance instRingWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [Ring α] : Ring (WithConv (Matrix m n α))

Equations

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

@[instance_reducible]

instance instCommRingWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [CommRing α] : CommRing (WithConv (Matrix m n α))

Equations

• instCommRingWithConvMatrix = { toRing := instRingWithConvMatrix, mul_comm := ⋯ }

@[instance_reducible]

instance instStarWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [Star α] : Star (WithConv (Matrix m n α))

Equations

• instStarWithConvMatrix = { star := fun (x : WithConv (Matrix m n α)) => WithConv.toConv (x.ofConv.map star) }

theorem intrinsicStar_def {α : Type u_1} {m : Type u_3} {n : Type u_4} [Star α] (x : WithConv (Matrix m n α)) : star x = WithConv.toConv (x.ofConv.map star)

@[instance_reducible]

instance instInvolutiveStarWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [InvolutiveStar α] : InvolutiveStar (WithConv (Matrix m n α))

Equations

• instInvolutiveStarWithConvMatrix = { toStar := instStarWithConvMatrix, star_involutive := ⋯ }

@[instance_reducible]

instance instStarAddMonoidWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [AddMonoid α] [StarAddMonoid α] : StarAddMonoid (WithConv (Matrix m n α))

Equations

• instStarAddMonoidWithConvMatrix = { toInvolutiveStar := instInvolutiveStarWithConvMatrix, star_add := ⋯ }

@[instance_reducible]

instance instStarMulWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [Mul α] [StarMul α] : StarMul (WithConv (Matrix m n α))

Equations

• instStarMulWithConvMatrix = { toInvolutiveStar := instInvolutiveStarWithConvMatrix, star_mul := ⋯ }

@[instance_reducible]

instance instStarRingWithConvMatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalNonAssocSemiring α] [StarRing α] : StarRing (WithConv (Matrix m n α))

Equations

• instStarRingWithConvMatrix = { toStarMul := instStarMulWithConvMatrix, star_add := ⋯ }

instance instSMulCommClassWithConvMatrix {α : Type u_1} {β : Type u_2} {m : Type u_3} {n : Type u_4} [Monoid β] [MulAction β α] [Mul α] [SMulCommClass β α α] : SMulCommClass β (WithConv (Matrix m n α)) (WithConv (Matrix m n α))

instance instIsScalarTowerWithConvMatrix {α : Type u_1} {β : Type u_2} {m : Type u_3} {n : Type u_4} [Monoid β] [MulAction β α] [Mul α] [IsScalarTower β α α] : IsScalarTower β (WithConv (Matrix m n α)) (WithConv (Matrix m n α))

@[instance_reducible]

instance instAlgebraWithConvMatrix {α : Type u_1} {β : Type u_2} {m : Type u_3} {n : Type u_4} [CommSemiring β] [Semiring α] [Algebra β α] : Algebra β (WithConv (Matrix m n α))

Equations

• instAlgebraWithConvMatrix = Algebra.ofModule ⋯ ⋯