case a.h
l : Type u_3
m : Type u_4
n : Type u_2
o : Type u_5
p : Type ?u.30648
q : Type ?u.30651
m' : o → Type ?u.30656
n' : o → Type ?u.30661
p' : o → Type ?u.30666
R : Type u_1
S : Type ?u.30672
α : Type ?u.30675
β : Type ?u.30678
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
i : n ⊕ o
j : l ⊕ m
⊢ (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-D) i j
l : Type u_3
m : Type u_4
n : Type u_2
o : Type u_5
p : Type ?u.30648
q : Type ?u.30651
m' : o → Type ?u.30656
n' : o → Type ?u.30661
p' : o → Type ?u.30666
R : Type u_1
S : Type ?u.30672
α : Type ?u.30675
β : Type ?u.30678
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
⊢ -fromBlocks A B C D = fromBlocks (-A) (-B) (-C) (-D)
ext i j
no goals
case a.h
l : Type u_3
m : Type u_4
n : Type u_2
o : Type u_5
p : Type ?u.30648
q : Type ?u.30651
m' : o → Type ?u.30656
n' : o → Type ?u.30661
p' : o → Type ?u.30666
R : Type u_1
S : Type ?u.30672
α : Type ?u.30675
β : Type ?u.30678
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
i : n ⊕ o
j : l ⊕ m
⊢ (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-D) i j
cases i <;> cases j <;> simp [fromBlocks]