case a.mk.h.mk
R : Type ?u.10684
α : Type u_6
α' : Type ?u.10690
β : Type u_1
β' : Type ?u.10696
γ : Type u_2
γ' : Type ?u.10702
l : Type u_4
m : Type u_5
n : Type u_3
p : Type ?u.10714
q : Type ?u.10717
r : Type ?u.10720
l' : Type ?u.10723
m' : Type ?u.10726
n' : Type ?u.10729
p' : Type ?u.10732
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
i₁ : l
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f A (diagonal b) (i₁, i₂) (j₁, j₂) = blockDiagonal (fun i => map A fun a => f a (b i)) (i₁, i₂) (j₁, j₂)
R : Type ?u.10684
α : Type u_6
α' : Type ?u.10690
β : Type u_1
β' : Type ?u.10696
γ : Type u_2
γ' : Type ?u.10702
l : Type u_4
m : Type u_5
n : Type u_3
p : Type ?u.10714
q : Type ?u.10717
r : Type ?u.10720
l' : Type ?u.10723
m' : Type ?u.10726
n' : Type ?u.10729
p' : Type ?u.10732
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
⊢ kroneckerMap f A (diagonal b) = blockDiagonal fun i => map A fun a => f a (b i)
ext (⟨i₁, i₂⟩⟨j₁, j₂⟩)
no goals
case a.mk.h.mk
R : Type ?u.10684
α : Type u_6
α' : Type ?u.10690
β : Type u_1
β' : Type ?u.10696
γ : Type u_2
γ' : Type ?u.10702
l : Type u_4
m : Type u_5
n : Type u_3
p : Type ?u.10714
q : Type ?u.10717
r : Type ?u.10720
l' : Type ?u.10723
m' : Type ?u.10726
n' : Type ?u.10729
p' : Type ?u.10732
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
i₁ : l
i₂ : n
j₁ : m
j₂ : n
⊢ kroneckerMap f A (diagonal b) (i₁, i₂) (j₁, j₂) = blockDiagonal (fun i => map A fun a => f a (b i)) (i₁, i₂) (j₁, j₂)
simp [diagonal, blockDiagonal, apply_ite (f (A i₁ j₁)), hf]