α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ IsSymm (Matrix.fromBlocks A B C D)
α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
⊢ IsSymm (Matrix.fromBlocks A B C D)
have hCB : Cᵀ = B := by
  rw [← hBC]
  simp
α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D
α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ IsSymm (Matrix.fromBlocks A B C D)
unfold Matrix.IsSymm
α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ (Matrix.fromBlocks A B C D)ᵀ = Matrix.fromBlocks A B C D
rw [fromBlocks_transpose]
α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
congr
no goals
α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
hCB : Cᵀ = B
⊢ Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
rw [hA, hCB, hBC, hD]
α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
⊢ Bᵀᵀ = B
α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
⊢ Cᵀ = B
rw [← hBC]
no goals
α : Type u_2
β : Type ?u.7912
n : Type u_3
m : Type u_1
R : Type ?u.7921
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : IsSymm A
hBC : Bᵀ = C
hD : IsSymm D
⊢ Bᵀᵀ = B
simp