Matrices over star rings. #
Notation #
The scope Matrix gives the following notation:
ᴴforMatrix.conjTranspose
The conjugate transpose of a matrix defined in term of star.
Instances For
@[simp]
theorem
Matrix.conjTranspose_single
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[DecidableEq m]
[AddMonoid α]
[StarAddMonoid α]
(i : m)
(j : n)
(a : α)
:
(single i j a).conjTranspose = single j i (star a)
@[simp]
theorem
Matrix.diagonal_conjTranspose
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[AddMonoid α]
[StarAddMonoid α]
(v : n → α)
:
(diagonal v).conjTranspose = diagonal (star v)
@[simp]
theorem
Matrix.diag_conjTranspose
{n : Type u_3}
{α : Type v}
[Star α]
(A : Matrix n n α)
:
A.conjTranspose.diag = star A.diag
theorem
Matrix.star_mulVec
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[NonUnitalSemiring α]
[Fintype n]
[StarRing α]
(M : Matrix m n α)
(v : n → α)
:
star (M.mulVec v) = vecMul (star v) M.conjTranspose
theorem
Matrix.star_vecMul
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[NonUnitalSemiring α]
[Fintype m]
[StarRing α]
(M : Matrix m n α)
(v : m → α)
:
star (vecMul v M) = M.conjTranspose.mulVec (star v)
theorem
Matrix.mulVec_conjTranspose
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[NonUnitalSemiring α]
[Fintype m]
[StarRing α]
(A : Matrix m n α)
(x : m → α)
:
A.conjTranspose.mulVec x = star (vecMul (star x) A)
theorem
Matrix.vecMul_conjTranspose
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[NonUnitalSemiring α]
[Fintype n]
[StarRing α]
(A : Matrix m n α)
(x : n → α)
:
vecMul x A.conjTranspose = star (A.mulVec (star x))
@[simp]
theorem
Matrix.conjTranspose_vecMulVec
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[Mul α]
[StarMul α]
(w : m → α)
(v : n → α)
:
(vecMulVec w v).conjTranspose = vecMulVec (star v) (star w)
@[simp]
theorem
Matrix.conjTranspose_apply
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[Star α]
(M : Matrix m n α)
(i : m)
(j : n)
:
M.conjTranspose j i = star (M i j)
Tell simp what the entries are in a conjugate transposed matrix.
Compare with mul_apply, diagonal_apply_eq, etc.
@[simp]
theorem
Matrix.conjTranspose_conjTranspose
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[InvolutiveStar α]
(M : Matrix m n α)
:
M.conjTranspose.conjTranspose = M
theorem
Matrix.conjTranspose_transpose
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[Star α]
(M : Matrix m n α)
:
M.conjTranspose.transpose = M.map star
theorem
Matrix.transpose_conjTranspose
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[Star α]
(M : Matrix m n α)
:
M.transpose.conjTranspose = M.map star
theorem
Matrix.conjTranspose_injective
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[InvolutiveStar α]
:
Function.Injective conjTranspose
@[simp]
theorem
Matrix.conjTranspose_inj
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[InvolutiveStar α]
{A B : Matrix m n α}
:
A.conjTranspose = B.conjTranspose ↔ A = B
@[simp]
theorem
Matrix.conjTranspose_eq_diagonal
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[AddMonoid α]
[StarAddMonoid α]
{M : Matrix n n α}
{v : n → α}
:
M.conjTranspose = diagonal v ↔ M = diagonal (star v)
@[simp]
theorem
Matrix.conjTranspose_zero
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddMonoid α]
[StarAddMonoid α]
:
conjTranspose 0 = 0
@[simp]
theorem
Matrix.conjTranspose_eq_zero
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddMonoid α]
[StarAddMonoid α]
{M : Matrix m n α}
:
M.conjTranspose = 0 ↔ M = 0
@[simp]
theorem
Matrix.conjTranspose_one
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[NonAssocSemiring α]
[StarRing α]
:
conjTranspose 1 = 1
@[simp]
theorem
Matrix.conjTranspose_eq_one
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[NonAssocSemiring α]
[StarRing α]
{M : Matrix n n α}
:
M.conjTranspose = 1 ↔ M = 1
@[simp]
theorem
Matrix.conjTranspose_natCast
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[NonAssocSemiring α]
[StarRing α]
(d : ℕ)
:
(↑d).conjTranspose = ↑d
@[simp]
theorem
Matrix.conjTranspose_eq_natCast
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[NonAssocSemiring α]
[StarRing α]
{M : Matrix n n α}
{d : ℕ}
:
M.conjTranspose = ↑d ↔ M = ↑d
@[simp]
theorem
Matrix.conjTranspose_ofNat
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[NonAssocSemiring α]
[StarRing α]
(d : ℕ)
[d.AtLeastTwo]
:
(OfNat.ofNat d).conjTranspose = OfNat.ofNat d
@[simp]
theorem
Matrix.conjTranspose_eq_ofNat
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[Semiring α]
[StarRing α]
{M : Matrix n n α}
{d : ℕ}
[d.AtLeastTwo]
:
M.conjTranspose = OfNat.ofNat d ↔ M = OfNat.ofNat d
@[simp]
theorem
Matrix.conjTranspose_intCast
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[Ring α]
[StarRing α]
(d : ℤ)
:
(↑d).conjTranspose = ↑d
@[simp]
theorem
Matrix.conjTranspose_eq_intCast
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[Ring α]
[StarRing α]
{M : Matrix n n α}
{d : ℤ}
:
M.conjTranspose = ↑d ↔ M = ↑d
@[simp]
theorem
Matrix.conjTranspose_add
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddMonoid α]
[StarAddMonoid α]
(M N : Matrix m n α)
:
(M + N).conjTranspose = M.conjTranspose + N.conjTranspose
@[simp]
theorem
Matrix.conjTranspose_sub
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddGroup α]
[StarAddMonoid α]
(M N : Matrix m n α)
:
(M - N).conjTranspose = M.conjTranspose - N.conjTranspose
@[simp]
theorem
Matrix.conjTranspose_smul
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Star R]
[Star α]
[SMul R α]
[StarModule R α]
(c : R)
(M : Matrix m n α)
:
(c • M).conjTranspose = star c • M.conjTranspose
Note that StarModule is quite a strong requirement; as such we also provide the following
variants which this lemma would not apply to:
@[simp]
theorem
Matrix.conjTranspose_smul_non_comm
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Star R]
[Star α]
[SMul R α]
[SMul Rᵐᵒᵖ α]
(c : R)
(M : Matrix m n α)
(h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a)
:
(c • M).conjTranspose = MulOpposite.op (star c) • M.conjTranspose
theorem
Matrix.conjTranspose_smul_self
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[Mul α]
[StarMul α]
(c : α)
(M : Matrix m n α)
:
(c • M).conjTranspose = MulOpposite.op (star c) • M.conjTranspose
theorem
Matrix.conjTranspose_nsmul
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddMonoid α]
[StarAddMonoid α]
(c : ℕ)
(M : Matrix m n α)
:
(c • M).conjTranspose = c • M.conjTranspose
theorem
Matrix.conjTranspose_zsmul
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddGroup α]
[StarAddMonoid α]
(c : ℤ)
(M : Matrix m n α)
:
(c • M).conjTranspose = c • M.conjTranspose
@[simp]
theorem
Matrix.conjTranspose_natCast_smul
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Semiring R]
[AddCommMonoid α]
[StarAddMonoid α]
[Module R α]
(c : ℕ)
(M : Matrix m n α)
:
(↑c • M).conjTranspose = ↑c • M.conjTranspose
@[simp]
theorem
Matrix.conjTranspose_ofNat_smul
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Semiring R]
[AddCommMonoid α]
[StarAddMonoid α]
[Module R α]
(c : ℕ)
[c.AtLeastTwo]
(M : Matrix m n α)
:
(OfNat.ofNat c • M).conjTranspose = OfNat.ofNat c • M.conjTranspose
@[simp]
theorem
Matrix.conjTranspose_intCast_smul
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Ring R]
[AddCommGroup α]
[StarAddMonoid α]
[Module R α]
(c : ℤ)
(M : Matrix m n α)
:
(↑c • M).conjTranspose = ↑c • M.conjTranspose
@[simp]
theorem
Matrix.conjTranspose_inv_natCast_smul
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[DivisionSemiring R]
[AddCommMonoid α]
[StarAddMonoid α]
[Module R α]
(c : ℕ)
(M : Matrix m n α)
:
((↑c)⁻¹ • M).conjTranspose = (↑c)⁻¹ • M.conjTranspose
@[simp]
theorem
Matrix.conjTranspose_inv_ofNat_smul
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[DivisionSemiring R]
[AddCommMonoid α]
[StarAddMonoid α]
[Module R α]
(c : ℕ)
[c.AtLeastTwo]
(M : Matrix m n α)
:
((OfNat.ofNat c)⁻¹ • M).conjTranspose = (OfNat.ofNat c)⁻¹ • M.conjTranspose
@[simp]
theorem
Matrix.conjTranspose_inv_intCast_smul
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[DivisionRing R]
[AddCommGroup α]
[StarAddMonoid α]
[Module R α]
(c : ℤ)
(M : Matrix m n α)
:
((↑c)⁻¹ • M).conjTranspose = (↑c)⁻¹ • M.conjTranspose
@[simp]
theorem
Matrix.conjTranspose_ratCast_smul
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[DivisionRing R]
[AddCommGroup α]
[StarAddMonoid α]
[Module R α]
(c : ℚ)
(M : Matrix m n α)
:
(↑c • M).conjTranspose = ↑c • M.conjTranspose
theorem
Matrix.conjTranspose_rat_smul
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddCommGroup α]
[StarAddMonoid α]
[Module ℚ α]
(c : ℚ)
(M : Matrix m n α)
:
(c • M).conjTranspose = c • M.conjTranspose
@[simp]
theorem
Matrix.conjTranspose_mul
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[Fintype n]
[NonUnitalNonAssocSemiring α]
[StarRing α]
(M : Matrix m n α)
(N : Matrix n l α)
:
(M * N).conjTranspose = N.conjTranspose * M.conjTranspose
@[simp]
theorem
Matrix.conjTranspose_neg
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddGroup α]
[StarAddMonoid α]
(M : Matrix m n α)
:
(-M).conjTranspose = -M.conjTranspose
theorem
Matrix.conjTranspose_map
{m : Type u_2}
{n : Type u_3}
{α : Type v}
{β : Type w}
[Star α]
[Star β]
{A : Matrix m n α}
(f : α → β)
(hf : Function.Semiconj f star star)
:
A.conjTranspose.map f = (A.map f).conjTranspose
@[simp]
theorem
Matrix.conjTranspose_eq_transpose_of_trivial
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[Star α]
[TrivialStar α]
(A : Matrix m n α)
:
A.conjTranspose = A.transpose
When star x = x on the coefficients (such as the real numbers) conjTranspose and transpose
are the same operation.
def
Matrix.conjTransposeAddEquiv
(m : Type u_2)
(n : Type u_3)
(α : Type v)
[AddMonoid α]
[StarAddMonoid α]
:
Matrix.conjTranspose as an AddEquiv
Instances For
@[simp]
theorem
Matrix.conjTransposeAddEquiv_apply
(m : Type u_2)
(n : Type u_3)
(α : Type v)
[AddMonoid α]
[StarAddMonoid α]
(M : Matrix m n α)
:
(conjTransposeAddEquiv m n α) M = M.conjTranspose
@[simp]
theorem
Matrix.conjTransposeAddEquiv_symm
(m : Type u_2)
(n : Type u_3)
(α : Type v)
[AddMonoid α]
[StarAddMonoid α]
:
(conjTransposeAddEquiv m n α).symm = conjTransposeAddEquiv n m α
theorem
Matrix.conjTranspose_list_sum
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddMonoid α]
[StarAddMonoid α]
(l : List (Matrix m n α))
:
l.sum.conjTranspose = (List.map conjTranspose l).sum
theorem
Matrix.conjTranspose_multiset_sum
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddCommMonoid α]
[StarAddMonoid α]
(s : Multiset (Matrix m n α))
:
s.sum.conjTranspose = (Multiset.map conjTranspose s).sum
theorem
Matrix.conjTranspose_sum
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddCommMonoid α]
[StarAddMonoid α]
{ι : Type u_10}
(s : Finset ι)
(M : ι → Matrix m n α)
:
(∑ i ∈ s, M i).conjTranspose = ∑ i ∈ s, (M i).conjTranspose
def
Matrix.conjTransposeLinearEquiv
(m : Type u_2)
(n : Type u_3)
(R : Type u_7)
(α : Type v)
[CommSemiring R]
[StarRing R]
[AddCommMonoid α]
[StarAddMonoid α]
[Module R α]
[StarModule R α]
:
Matrix.conjTranspose as a LinearMap
Instances For
@[simp]
theorem
Matrix.conjTransposeLinearEquiv_apply
(m : Type u_2)
(n : Type u_3)
(R : Type u_7)
(α : Type v)
[CommSemiring R]
[StarRing R]
[AddCommMonoid α]
[StarAddMonoid α]
[Module R α]
[StarModule R α]
(a✝ : Matrix m n α)
:
(conjTransposeLinearEquiv m n R α) a✝ = (conjTransposeAddEquiv m n α).toFun a✝
@[simp]
theorem
Matrix.conjTransposeLinearEquiv_symm
(m : Type u_2)
(n : Type u_3)
(R : Type u_7)
(α : Type v)
[CommSemiring R]
[StarRing R]
[AddCommMonoid α]
[StarAddMonoid α]
[Module R α]
[StarModule R α]
:
(conjTransposeLinearEquiv m n R α).symm = conjTransposeLinearEquiv n m R α
def
Matrix.conjTransposeRingEquiv
(m : Type u_2)
(α : Type v)
[NonUnitalNonAssocSemiring α]
[StarRing α]
[Fintype m]
:
Matrix.conjTranspose as a RingEquiv to the opposite ring
Instances For
@[simp]
theorem
Matrix.conjTransposeRingEquiv_apply
(m : Type u_2)
(α : Type v)
[NonUnitalNonAssocSemiring α]
[StarRing α]
[Fintype m]
(a✝ : Matrix m m α)
:
(conjTransposeRingEquiv m α) a✝ = MulOpposite.op a✝.conjTranspose
@[simp]
theorem
Matrix.conjTransposeRingEquiv_symm_apply
(m : Type u_2)
(α : Type v)
[NonUnitalNonAssocSemiring α]
[StarRing α]
[Fintype m]
(a✝ : (Matrix m m α)ᵐᵒᵖ)
:
(conjTransposeRingEquiv m α).symm a✝ = (MulOpposite.unop a✝).conjTranspose
@[simp]
theorem
Matrix.conjTranspose_pow
{m : Type u_2}
{α : Type v}
[Semiring α]
[StarRing α]
[Fintype m]
[DecidableEq m]
(M : Matrix m m α)
(k : ℕ)
:
(M ^ k).conjTranspose = M.conjTranspose ^ k
theorem
Matrix.conjTranspose_list_prod
{m : Type u_2}
{α : Type v}
[Semiring α]
[StarRing α]
[Fintype m]
[DecidableEq m]
(l : List (Matrix m m α))
:
l.prod.conjTranspose = (List.map conjTranspose l).reverse.prod
@[implicit_reducible]
When α has a star operation, square matrices Matrix n n α have a star
operation equal to Matrix.conjTranspose.
theorem
Matrix.star_eq_conjTranspose
{m : Type u_2}
{α : Type v}
[Star α]
(M : Matrix m m α)
:
star M = M.conjTranspose
@[simp]
@[implicit_reducible]
instance
Matrix.instInvolutiveStar
{n : Type u_3}
{α : Type v}
[InvolutiveStar α]
:
InvolutiveStar (Matrix n n α)
@[implicit_reducible]
instance
Matrix.instStarAddMonoid
{n : Type u_3}
{α : Type v}
[AddMonoid α]
[StarAddMonoid α]
:
StarAddMonoid (Matrix n n α)
When α is a *-additive monoid, Matrix.star is also a *-additive monoid.
instance
Matrix.instStarModule
{n : Type u_3}
{α : Type v}
{β : Type w}
[Star α]
[Star β]
[SMul α β]
[StarModule α β]
:
StarModule α (Matrix n n β)
@[implicit_reducible]
instance
Matrix.instStarRing
{n : Type u_3}
{α : Type v}
[Fintype n]
[NonUnitalSemiring α]
[StarRing α]
:
When α is a *-(semi)ring, Matrix.star is also a *-(semi)ring.
theorem
Matrix.star_mul
{n : Type u_3}
{α : Type v}
[Fintype n]
[NonUnitalNonAssocSemiring α]
[StarRing α]
(M N : Matrix n n α)
:
A version of star_mul for * instead of *.
@[simp]
theorem
Matrix.conjTranspose_submatrix
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type v}
[Star α]
(A : Matrix m n α)
(r : l → m)
(c : o → n)
:
(A.submatrix r c).conjTranspose = A.conjTranspose.submatrix c r
theorem
Matrix.conjTranspose_reindex
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type v}
[Star α]
(eₘ : m ≃ l)
(eₙ : n ≃ o)
(M : Matrix m n α)
:
((reindex eₘ eₙ) M).conjTranspose = (reindex eₙ eₘ) M.conjTranspose