α : Type u_2
β : Type ?u.5694
m : Type u_1
n : Type u_3
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
hCB : Cᴴ = B
⊢ IsHermitian (Matrix.fromBlocks A B C D)
α : Type u_2
β : Type ?u.5694
m : Type u_1
n : Type u_3
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
⊢ IsHermitian (Matrix.fromBlocks A B C D)
have hCB : Cᴴ = B := by rw [← hBC, conjTranspose_conjTranspose]
α : Type u_2
β : Type ?u.5694
m : Type u_1
n : Type u_3
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
hCB : Cᴴ = B
⊢ (Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks A B C D
α : Type u_2
β : Type ?u.5694
m : Type u_1
n : Type u_3
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
hCB : Cᴴ = B
⊢ IsHermitian (Matrix.fromBlocks A B C D)
unfold Matrix.IsHermitian
no goals
α : Type u_2
β : Type ?u.5694
m : Type u_1
n : Type u_3
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
hCB : Cᴴ = B
⊢ (Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks A B C D
rw [fromBlocks_conjTranspose, hBC, hCB, hA, hD]
no goals
α : Type u_2
β : Type ?u.5694
m : Type u_1
n : Type u_3
A✝ : Matrix n n α
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsHermitian A
hBC : Bᴴ = C
hD : IsHermitian D
⊢ Cᴴ = B
rw [← hBC, conjTranspose_conjTranspose]