exact (hX _ _).mul (hY _ _)
ι : Type ?u.17223
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.17238
q : Type ?u.17241
inst✝¹⁰ : Fintype m
inst✝⁹ : Fintype n
inst✝⁸ : Fintype p
inst✝⁷ : Fintype q
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : NontriviallyNormedField R
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra R A
X Y : R → Matrix m n A
X' Y' : Matrix m n A
r : R
hX : ∀ (i : m) (j : n), HasDerivAt (fun r => X r i j) (X' i j) r
hY : ∀ (i : m) (j : n), HasDerivAt (fun r => Y r i j) (Y' i j) r
i : m
j : n
⊢ HasDerivAt (fun r => (X r ⊙ Y r) i j) ((X' ⊙ Y r + X r ⊙ Y') i j) r
no goals