case a.h
l : Type u_4
m : Type u_5
n : Type u_3
o : Type u_6
p : Type ?u.23629
q : Type ?u.23632
m' : o → Type ?u.23637
n' : o → Type ?u.23642
p' : o → Type ?u.23647
R : Type u_1
S : Type ?u.23653
α : Type u_2
β : Type ?u.23659
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j
l : Type u_4
m : Type u_5
n : Type u_3
o : Type u_6
p : Type ?u.23629
q : Type ?u.23632
m' : o → Type ?u.23637
n' : o → Type ?u.23642
p' : o → Type ?u.23647
R : Type u_1
S : Type ?u.23653
α : Type u_2
β : Type ?u.23659
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ x • fromBlocks A B C D = fromBlocks (x • A) (x • B) (x • C) (x • D)
ext (i j)
no goals
case a.h
l : Type u_4
m : Type u_5
n : Type u_3
o : Type u_6
p : Type ?u.23629
q : Type ?u.23632
m' : o → Type ?u.23637
n' : o → Type ?u.23642
p' : o → Type ?u.23647
R : Type u_1
S : Type ?u.23653
α : Type u_2
β : Type ?u.23659
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks]