intro i
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i : m
j : n
⊢ ∀ (i_1 : n), DifferentiableAt R (fun x => f x i i_1) r
case a
ι : Type ?u.28262
R : Type u_4
A : Type u_3
m : Type u_1
n : Type u_2
p : Type ?u.28277
q : Type ?u.28280
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
f : R → Matrix m n A
r : R
hX : DifferentiableAt R f r
i✝ : m
j i : n
⊢ DifferentiableAt R (fun x => f x i✝ i) r