case a
l : Type ?u.28777
m : Type u_1
n : Type u_2
o : Type ?u.28786
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ map (M - N) (fun i j => ↑f) i✝ j✝ = ((map M fun i j => ↑f) - map N fun i j => ↑f) i✝ j✝
l : Type ?u.28777
m : Type u_1
n : Type u_2
o : Type ?u.28786
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
⊢ (map (M - N) fun i j => ↑f) = (map M fun i j => ↑f) - map N fun i j => ↑f
ext
no goals
case a
l : Type ?u.28777
m : Type u_1
n : Type u_2
o : Type ?u.28786
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ map (M - N) (fun i j => ↑f) i✝ j✝ = ((map M fun i j => ↑f) - map N fun i j => ↑f) i✝ j✝
simp