Matrices over star rings. #

Notation #

The locale Matrix gives the following notation:

ᴴ for Matrix.conjTranspose

source

def Matrix.conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} [Star α] (M : Matrix m n α) :

Matrix n m α

The conjugate transpose of a matrix defined in term of star.

Equations

M.conjTranspose = M.transpose.map star

Instances For

source

def Matrix.«term_ᴴ» :

Lean.TrailingParserDescr

The conjugate transpose of a matrix defined in term of star.

Equations

Matrix.«term_ᴴ» = Lean.ParserDescr.trailingNode `Matrix.«term_ᴴ» 1024 1024 (Lean.ParserDescr.symbol "ᴴ")

Instances For

source

@[simp]

theorem Matrix.diagonal_conjTranspose {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoid α] [StarAddMonoid α] (v : n → α) :

(Matrix.diagonal v).conjTranspose = Matrix.diagonal (star v)

source

@[simp]

theorem Matrix.diag_conjTranspose {n : Type u_3} {α : Type v} [AddMonoid α] [StarAddMonoid α] (A : Matrix n n α) :

A.conjTranspose.diag = star A.diag

source

theorem Matrix.star_dotProduct_star {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalSemiring α] [StarRing α] (v : m → α) (w : m → α) :

Matrix.dotProduct (star v) (star w) = star (Matrix.dotProduct w v)

source

theorem Matrix.star_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalSemiring α] [StarRing α] (v : m → α) (w : m → α) :

Matrix.dotProduct (star v) w = star (Matrix.dotProduct (star w) v)

source

theorem Matrix.dotProduct_star {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalSemiring α] [StarRing α] (v : m → α) (w : m → α) :

Matrix.dotProduct v (star w) = star (Matrix.dotProduct w (star v))

source

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) = Matrix.vecMul (star v) M.conjTranspose

source

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 (Matrix.vecMul v M) = M.conjTranspose.mulVec (star v)

source

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 (Matrix.vecMul (star x) A)

source

theorem Matrix.vecMul_conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] [StarRing α] (A : Matrix m n α) (x : n → α) :

Matrix.vecMul x A.conjTranspose = star (A.mulVec (star x))

source

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

source

@[simp]

theorem Matrix.conjTranspose_conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} [InvolutiveStar α] (M : Matrix m n α) :

M.conjTranspose.conjTranspose = M

source

theorem Matrix.conjTranspose_injective {m : Type u_2} {n : Type u_3} {α : Type v} [InvolutiveStar α] :

Function.Injective Matrix.conjTranspose

source

@[simp]

theorem Matrix.conjTranspose_inj {m : Type u_2} {n : Type u_3} {α : Type v} [InvolutiveStar α] {A : Matrix m n α} {B : Matrix m n α} :

A.conjTranspose = B.conjTranspose ↔ A = B

source

@[simp]

theorem Matrix.conjTranspose_eq_diagonal {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoid α] [StarAddMonoid α] {M : Matrix n n α} {v : n → α} :

M.conjTranspose = Matrix.diagonal v ↔ M = Matrix.diagonal (star v)

source

@[simp]

theorem Matrix.conjTranspose_zero {m : Type u_2} {n : Type u_3} {α : Type v} [AddMonoid α] [StarAddMonoid α] :

Matrix.conjTranspose 0 = 0

source

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

source

@[simp]

theorem Matrix.conjTranspose_one {n : Type u_3} {α : Type v} [DecidableEq n] [Semiring α] [StarRing α] :

Matrix.conjTranspose 1 = 1

source

@[simp]

theorem Matrix.conjTranspose_eq_one {n : Type u_3} {α : Type v} [DecidableEq n] [Semiring α] [StarRing α] {M : Matrix n n α} :

M.conjTranspose = 1 ↔ M = 1

source

@[simp]

theorem Matrix.conjTranspose_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [Semiring α] [StarRing α] (d : ℕ) :

(↑d).conjTranspose = ↑d

source

@[simp]

theorem Matrix.conjTranspose_eq_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [Semiring α] [StarRing α] {M : Matrix n n α} {d : ℕ} :

M.conjTranspose = ↑d ↔ M = ↑d

source

@[simp]

theorem Matrix.conjTranspose_ofNat {n : Type u_3} {α : Type v} [DecidableEq n] [Semiring α] [StarRing α] (d : ℕ) [d.AtLeastTwo] :

(OfNat.ofNat d).conjTranspose = OfNat.ofNat d

source

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

source

@[simp]

theorem Matrix.conjTranspose_intCast {n : Type u_3} {α : Type v} [DecidableEq n] [Ring α] [StarRing α] (d : ℤ) :

(↑d).conjTranspose = ↑d

source

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

source

@[simp]

theorem Matrix.conjTranspose_add {m : Type u_2} {n : Type u_3} {α : Type v} [AddMonoid α] [StarAddMonoid α] (M : Matrix m n α) (N : Matrix m n α) :

(M + N).conjTranspose = M.conjTranspose + N.conjTranspose

source

@[simp]

theorem Matrix.conjTranspose_sub {m : Type u_2} {n : Type u_3} {α : Type v} [AddGroup α] [StarAddMonoid α] (M : Matrix m n α) (N : Matrix m n α) :

(M - N).conjTranspose = M.conjTranspose - N.conjTranspose

source

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

source

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

source

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

source

@[simp]

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

source

@[simp]

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[simp]

theorem Matrix.conjTranspose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype n] [NonUnitalSemiring α] [StarRing α] (M : Matrix m n α) (N : Matrix n l α) :

(M * N).conjTranspose = N.conjTranspose * M.conjTranspose

source

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

source

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

source

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

source

def Matrix.conjTransposeAddEquiv (m : Type u_2) (n : Type u_3) (α : Type v) [AddMonoid α] [StarAddMonoid α] :

Matrix m n α ≃+ Matrix n m α

Matrix.conjTranspose as an AddEquiv

Equations

Matrix.conjTransposeAddEquiv m n α = { toFun := Matrix.conjTranspose, invFun := Matrix.conjTranspose, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem Matrix.conjTransposeAddEquiv_apply (m : Type u_2) (n : Type u_3) (α : Type v) [AddMonoid α] [StarAddMonoid α] (M : Matrix m n α) :

(Matrix.conjTransposeAddEquiv m n α) M = M.conjTranspose

source

@[simp]

theorem Matrix.conjTransposeAddEquiv_symm (m : Type u_2) (n : Type u_3) (α : Type v) [AddMonoid α] [StarAddMonoid α] :

(Matrix.conjTransposeAddEquiv m n α).symm = Matrix.conjTransposeAddEquiv n m α

source

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 Matrix.conjTranspose l).sum

source

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 Matrix.conjTranspose s).sum

source

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

source

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 m n α ≃ₗ⋆[R] Matrix n m α

Matrix.conjTranspose as a LinearMap

Equations

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

Instances For

source

@[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 α), (Matrix.conjTransposeLinearEquiv m n R α) a = (Matrix.conjTransposeAddEquiv m n α).toFun a

source

@[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 α] :

(Matrix.conjTransposeLinearEquiv m n R α).symm = Matrix.conjTransposeLinearEquiv n m R α

source

def Matrix.conjTransposeRingEquiv (m : Type u_2) (α : Type v) [Semiring α] [StarRing α] [Fintype m] :

Matrix m m α ≃+* (Matrix m m α)ᵐᵒᵖ

Matrix.conjTranspose as a RingEquiv to the opposite ring

Equations

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

Instances For

source

@[simp]

theorem Matrix.conjTransposeRingEquiv_symm_apply (m : Type u_2) (α : Type v) [Semiring α] [StarRing α] [Fintype m] (M : (Matrix m m α)ᵐᵒᵖ) :

(Matrix.conjTransposeRingEquiv m α).symm M = (MulOpposite.unop M).conjTranspose

source

@[simp]

theorem Matrix.conjTransposeRingEquiv_apply (m : Type u_2) (α : Type v) [Semiring α] [StarRing α] [Fintype m] (M : Matrix m m α) :

(Matrix.conjTransposeRingEquiv m α) M = MulOpposite.op M.conjTranspose

source

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

source

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 Matrix.conjTranspose l).reverse.prod

source

instance Matrix.instStar {n : Type u_3} {α : Type v} [Star α] :

Star (Matrix n n α)

When α has a star operation, square matrices Matrix n n α have a star operation equal to Matrix.conjTranspose.

Equations

Matrix.instStar = { star := Matrix.conjTranspose }

source

theorem Matrix.star_eq_conjTranspose {m : Type u_2} {α : Type v} [Star α] (M : Matrix m m α) :

star M = M.conjTranspose

source

@[simp]

theorem Matrix.star_apply {n : Type u_3} {α : Type v} [Star α] (M : Matrix n n α) (i : n) (j : n) :

star M i j = star (M j i)

source

instance Matrix.instInvolutiveStar {n : Type u_3} {α : Type v} [InvolutiveStar α] :

InvolutiveStar (Matrix n n α)

Equations

Matrix.instInvolutiveStar = InvolutiveStar.mk ⋯

source

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.

Equations

Matrix.instStarAddMonoid = StarAddMonoid.mk ⋯

source

instance Matrix.instStarModule {n : Type u_3} {α : Type v} {β : Type w} [Star α] [Star β] [SMul α β] [StarModule α β] :

StarModule α (Matrix n n β)

Equations

⋯ = ⋯

source

instance Matrix.instStarRing {n : Type u_3} {α : Type v} [Fintype n] [NonUnitalSemiring α] [StarRing α] :

StarRing (Matrix n n α)

When α is a *-(semi)ring, Matrix.star is also a *-(semi)ring.

Equations

Matrix.instStarRing = StarRing.mk ⋯

source

theorem Matrix.star_mul {n : Type u_3} {α : Type v} [Fintype n] [NonUnitalSemiring α] [StarRing α] (M : Matrix n n α) (N : Matrix n n α) :

star (M * N) = star N * star M

A version of star_mul for * instead of *.

source

@[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_reindex : l → m) (c_reindex : o → n) :

(A.submatrix r_reindex c_reindex).conjTranspose = A.conjTranspose.submatrix c_reindex r_reindex

source

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 α) :

((Matrix.reindex eₘ eₙ) M).conjTranspose = (Matrix.reindex eₙ eₘ) M.conjTranspose

Documentation

Mathlib.Data.Matrix.ConjTranspose

Matrices over star rings. #

Notation #