m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ σ : Perm n, ↑↑(↑sign σ) * ∏ i : n, Mᵀ (↑σ i) i = ∑ σ : Perm n, ↑↑(↑sign σ) * ∏ i : n, M (↑σ i) i
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ det Mᵀ = det M
rw [det_apply', det_apply']
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∀ (x : Perm n), ↑↑(↑sign x) * ∏ i : n, Mᵀ (↑x i) i = ↑↑(↑sign x⁻¹) * ∏ i : n, M (↑x⁻¹ i) i
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ σ : Perm n, ↑↑(↑sign σ) * ∏ i : n, Mᵀ (↑σ i) i = ∑ σ : Perm n, ↑↑(↑sign σ) * ∏ i : n, M (↑σ i) i
refine' Fintype.sum_bijective _ inv_involutive.bijective _ _ _
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ↑↑(↑sign σ) * ∏ i : n, Mᵀ (↑σ i) i = ↑↑(↑sign σ⁻¹) * ∏ i : n, M (↑σ⁻¹ i) i
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∀ (x : Perm n), ↑↑(↑sign x) * ∏ i : n, Mᵀ (↑x i) i = ↑↑(↑sign x⁻¹) * ∏ i : n, M (↑x⁻¹ i) i
intro σ
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ↑↑(↑sign σ) * ∏ i : n, Mᵀ (↑σ i) i = ↑↑(↑sign σ) * ∏ i : n, M (↑σ⁻¹ i) i
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ↑↑(↑sign σ) * ∏ i : n, Mᵀ (↑σ i) i = ↑↑(↑sign σ⁻¹) * ∏ i : n, M (↑σ⁻¹ i) i
rw [sign_inv]
case e_a
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ∏ i : n, Mᵀ (↑σ i) i = ∏ i : n, M (↑σ⁻¹ i) i
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ↑↑(↑sign σ) * ∏ i : n, Mᵀ (↑σ i) i = ↑↑(↑sign σ) * ∏ i : n, M (↑σ⁻¹ i) i
congr 1
case e_a.h
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ∀ (x : n), Mᵀ (↑σ x) x = M (↑σ⁻¹ (↑σ x)) (↑σ x)
case e_a
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ∏ i : n, Mᵀ (↑σ i) i = ∏ i : n, M (↑σ⁻¹ i) i
apply Fintype.prod_equiv σ
case e_a.h
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
x✝ : n
⊢ Mᵀ (↑σ x✝) x✝ = M (↑σ⁻¹ (↑σ x✝)) (↑σ x✝)
case e_a.h
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ∀ (x : n), Mᵀ (↑σ x) x = M (↑σ⁻¹ (↑σ x)) (↑σ x)
intros
no goals
case e_a.h
m : Type ?u.1055285
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
x✝ : n
⊢ Mᵀ (↑σ x✝) x✝ = M (↑σ⁻¹ (↑σ x✝)) (↑σ x✝)
simp