l : Type ?u.201579
m : Type ?u.201582
n : Type ?u.201585
o : Type u_4
p : Type ?u.201591
q : Type ?u.201594
m' : o → Type u_2
n' : o → Type u_3
p' : o → Type ?u.201609
R : Type ?u.201612
S : Type ?u.201615
α✝ : Type ?u.201618
β : Type ?u.201621
inst✝⁴ : DecidableEq o
inst✝³ : Zero α✝
inst✝² : Zero β
α : Type u_1
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ map (blockDiagonal' fun k => (M k)ᵀ) star = blockDiagonal' fun k => map (M k)ᵀ star
l : Type ?u.201579
m : Type ?u.201582
n : Type ?u.201585
o : Type u_4
p : Type ?u.201591
q : Type ?u.201594
m' : o → Type u_2
n' : o → Type u_3
p' : o → Type ?u.201609
R : Type ?u.201612
S : Type ?u.201615
α✝ : Type ?u.201618
β : Type ?u.201621
inst✝⁴ : DecidableEq o
inst✝³ : Zero α✝
inst✝² : Zero β
α : Type u_1
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ (blockDiagonal' M)ᴴ = blockDiagonal' fun k => (M k)ᴴ
simp only [conjTranspose, blockDiagonal'_transpose]
no goals
l : Type ?u.201579
m : Type ?u.201582
n : Type ?u.201585
o : Type u_4
p : Type ?u.201591
q : Type ?u.201594
m' : o → Type u_2
n' : o → Type u_3
p' : o → Type ?u.201609
R : Type ?u.201612
S : Type ?u.201615
α✝ : Type ?u.201618
β : Type ?u.201621
inst✝⁴ : DecidableEq o
inst✝³ : Zero α✝
inst✝² : Zero β
α : Type u_1
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ map (blockDiagonal' fun k => (M k)ᵀ) star = blockDiagonal' fun k => map (M k)ᵀ star
exact blockDiagonal'_map _ star (star_zero α)