X : Type u_3
α : Type ?u.24141
l : Type ?u.24144
m : Type ?u.24147
n : Type u_1
p : Type ?u.24153
S : Type ?u.24156
R : Type u_2
m' : l → Type ?u.24164
n' : l → Type ?u.24169
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : TopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x =>
    Finset.sum Finset.univ fun x_1 => ↑Equiv.Perm.sign x_1 • Finset.prod Finset.univ fun x_2 => A x (↑x_1 x_2) x_2
X : Type u_3
α : Type ?u.24141
l : Type ?u.24144
m : Type ?u.24147
n : Type u_1
p : Type ?u.24153
S : Type ?u.24156
R : Type u_2
m' : l → Type ?u.24164
n' : l → Type ?u.24169
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : TopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x => det (A x)
simp_rw [Matrix.det_apply]
X : Type u_3
α : Type ?u.24141
l✝ : Type ?u.24144
m : Type ?u.24147
n : Type u_1
p : Type ?u.24153
S : Type ?u.24156
R : Type u_2
m' : l✝ → Type ?u.24164
n' : l✝ → Type ?u.24169
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : TopologicalRing R
A : X → Matrix n n R
hA : Continuous A
l : Equiv.Perm n
x✝ : l ∈ Finset.univ
⊢ Continuous fun x => Finset.prod Finset.univ fun x_1 => A x (↑l x_1) x_1
X : Type u_3
α : Type ?u.24141
l : Type ?u.24144
m : Type ?u.24147
n : Type u_1
p : Type ?u.24153
S : Type ?u.24156
R : Type u_2
m' : l → Type ?u.24164
n' : l → Type ?u.24169
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : TopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x =>
    Finset.sum Finset.univ fun x_1 => ↑Equiv.Perm.sign x_1 • Finset.prod Finset.univ fun x_2 => A x (↑x_1 x_2) x_2
refine' continuous_finset_sum _ fun l _ => Continuous.const_smul _ _
no goals
X : Type u_3
α : Type ?u.24141
l✝ : Type ?u.24144
m : Type ?u.24147
n : Type u_1
p : Type ?u.24153
S : Type ?u.24156
R : Type u_2
m' : l✝ → Type ?u.24164
n' : l✝ → Type ?u.24169
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : TopologicalRing R
A : X → Matrix n n R
hA : Continuous A
l : Equiv.Perm n
x✝ : l ∈ Finset.univ
⊢ Continuous fun x => Finset.prod Finset.univ fun x_1 => A x (↑l x_1) x_1
refine' continuous_finset_prod _ fun l _ => hA.matrix_elem _ _