R : Type u_3
A : Type u_2
B : Type ?u.807401
S : Type ?u.807404
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : CommRing S
inst✝³ : Algebra R A
inst✝² : Algebra R B
f : R →+* S
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral R (∑ σ : Equiv.Perm n, ↑Equiv.Perm.sign σ • ∏ i : n, M (↑σ i) i)
R : Type u_3
A : Type u_2
B : Type ?u.807401
S : Type ?u.807404
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : CommRing S
inst✝³ : Algebra R A
inst✝² : Algebra R B
f : R →+* S
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral R (Matrix.det M)
rw [Matrix.det_apply]
no goals
R : Type u_3
A : Type u_2
B : Type ?u.807401
S : Type ?u.807404
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : CommRing S
inst✝³ : Algebra R A
inst✝² : Algebra R B
f : R →+* S
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n A
h : ∀ (i j : n), IsIntegral R (M i j)
⊢ IsIntegral R (∑ σ : Equiv.Perm n, ↑Equiv.Perm.sign σ • ∏ i : n, M (↑σ i) i)
exact IsIntegral.sum _ fun σ _hσ => IsIntegral.zsmul (IsIntegral.prod _ fun i _hi => h _ _) _