m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
⊢ det A =
    (-1) ^ ↑i * ∑ x : Fin (Nat.succ n), (-1) ^ ↑x * (A i x * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove x)))
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
⊢ det A = ∑ j : Fin (Nat.succ n), (-1) ^ (↑i + ↑j) * A i j * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove j))
simp_rw [pow_add, mul_assoc, ← mul_sum]
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
⊢ det A =
    (-1) ^ ↑i * ∑ x : Fin (Nat.succ n), (-1) ^ ↑x * (A i x * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove x)))
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
⊢ det A =
    (-1) ^ ↑i * ∑ x : Fin (Nat.succ n), (-1) ^ ↑x * (A i x * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove x)))
have : det A = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by
  calc
    det A = ↑((-1 : ℤˣ) ^ (i : ℕ) * (-1 : ℤˣ) ^ (i : ℕ) : ℤˣ) * det A := by simp
    _ = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by simp [-Int.units_mul_self]
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
⊢ (-1) ^ ↑i * (↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A) =
    (-1) ^ ↑i * ∑ x : Fin (Nat.succ n), (-1) ^ ↑x * (A i x * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove x)))
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
⊢ det A =
    (-1) ^ ↑i * ∑ x : Fin (Nat.succ n), (-1) ^ ↑x * (A i x * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove x)))
rw [this, mul_assoc]
case e_a
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
⊢ ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A =
    ∑ x : Fin (Nat.succ n), (-1) ^ ↑x * (A i x * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove x)))
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
⊢ (-1) ^ ↑i * (↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A) =
    (-1) ^ ↑i * ∑ x : Fin (Nat.succ n), (-1) ^ ↑x * (A i x * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove x)))
congr
case e_a
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
⊢ ∑ j : Fin (Nat.succ n),
      (-1) ^ ↑j * A (↑(Fin.cycleRange i)⁻¹ 0) j *
        det (submatrix (fun i_1 => A (↑(Fin.cycleRange i)⁻¹ i_1)) Fin.succ ↑(Fin.succAbove j)) =
    ∑ x : Fin (Nat.succ n), (-1) ^ ↑x * (A i x * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove x)))
case e_a
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
⊢ ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A =
    ∑ x : Fin (Nat.succ n), (-1) ^ ↑x * (A i x * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove x)))
rw [← det_permute, det_succ_row_zero]
case e_a
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
j : Fin (Nat.succ n)
x✝ : j ∈ univ
⊢ (-1) ^ ↑j * A (↑(Fin.cycleRange i)⁻¹ 0) j *
      det (submatrix (fun i_1 => A (↑(Fin.cycleRange i)⁻¹ i_1)) Fin.succ ↑(Fin.succAbove j)) =
    (-1) ^ ↑j * (A i j * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove j)))
case e_a
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
⊢ ∑ j : Fin (Nat.succ n),
      (-1) ^ ↑j * A (↑(Fin.cycleRange i)⁻¹ 0) j *
        det (submatrix (fun i_1 => A (↑(Fin.cycleRange i)⁻¹ i_1)) Fin.succ ↑(Fin.succAbove j)) =
    ∑ x : Fin (Nat.succ n), (-1) ^ ↑x * (A i x * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove x)))
refine' Finset.sum_congr rfl fun j _ => _
case e_a
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
j : Fin (Nat.succ n)
x✝ : j ∈ univ
⊢ (-1) ^ ↑j *
      (A (↑(Fin.cycleRange i)⁻¹ 0) j *
        det (↑of fun i_1 j_1 => A (↑(Fin.cycleRange i)⁻¹ (Fin.succ i_1)) (↑(Fin.succAbove j) j_1))) =
    (-1) ^ ↑j * (A i j * det (↑of fun i_1 j_1 => A (↑(Fin.succAbove i) i_1) (↑(Fin.succAbove j) j_1)))
case e_a
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
j : Fin (Nat.succ n)
x✝ : j ∈ univ
⊢ (-1) ^ ↑j * A (↑(Fin.cycleRange i)⁻¹ 0) j *
      det (submatrix (fun i_1 => A (↑(Fin.cycleRange i)⁻¹ i_1)) Fin.succ ↑(Fin.succAbove j)) =
    (-1) ^ ↑j * (A i j * det (submatrix A ↑(Fin.succAbove i) ↑(Fin.succAbove j)))
rw [mul_assoc, Matrix.submatrix, Matrix.submatrix]
case e_a.e_a.e_a.e_a
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
j : Fin (Nat.succ n)
x✝ : j ∈ univ
⊢ ↑(Fin.cycleRange i)⁻¹ 0 = i

case e_a.e_a.e_a.e_M.h.e_6.h
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
j : Fin (Nat.succ n)
x✝ : j ∈ univ
⊢ (fun i_1 j_1 => A (↑(Fin.cycleRange i)⁻¹ (Fin.succ i_1)) (↑(Fin.succAbove j) j_1)) = fun i_1 j_1 =>
    A (↑(Fin.succAbove i) i_1) (↑(Fin.succAbove j) j_1)
case e_a
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
j : Fin (Nat.succ n)
x✝ : j ∈ univ
⊢ (-1) ^ ↑j *
      (A (↑(Fin.cycleRange i)⁻¹ 0) j *
        det (↑of fun i_1 j_1 => A (↑(Fin.cycleRange i)⁻¹ (Fin.succ i_1)) (↑(Fin.succAbove j) j_1))) =
    (-1) ^ ↑j * (A i j * det (↑of fun i_1 j_1 => A (↑(Fin.succAbove i) i_1) (↑(Fin.succAbove j) j_1)))
congr
no goals
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
⊢ det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
calc
  det A = ↑((-1 : ℤˣ) ^ (i : ℕ) * (-1 : ℤˣ) ^ (i : ℕ) : ℤˣ) * det A := by simp
  _ = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by simp [-Int.units_mul_self]
no goals
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
⊢ det A = ↑↑((-1) ^ ↑i * (-1) ^ ↑i) * det A
simp
no goals
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
⊢ ↑↑((-1) ^ ↑i * (-1) ^ ↑i) * det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
simp [-Int.units_mul_self]
no goals
case e_a.e_a.e_a.e_a
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
j : Fin (Nat.succ n)
x✝ : j ∈ univ
⊢ ↑(Fin.cycleRange i)⁻¹ 0 = i
rw [Equiv.Perm.inv_def, Fin.cycleRange_symm_zero]
case e_a.e_a.e_a.e_M.h.e_6.h.h.h
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
j : Fin (Nat.succ n)
x✝ : j ∈ univ
i' j' : Fin n
⊢ A (↑(Fin.cycleRange i)⁻¹ (Fin.succ i')) (↑(Fin.succAbove j) j') = A (↑(Fin.succAbove i) i') (↑(Fin.succAbove j) j')
case e_a.e_a.e_a.e_M.h.e_6.h
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
j : Fin (Nat.succ n)
x✝ : j ∈ univ
⊢ (fun i_1 j_1 => A (↑(Fin.cycleRange i)⁻¹ (Fin.succ i_1)) (↑(Fin.succAbove j) j_1)) = fun i_1 j_1 =>
    A (↑(Fin.succAbove i) i_1) (↑(Fin.succAbove j) j_1)
ext (i' j')
no goals
case e_a.e_a.e_a.e_M.h.e_6.h.h.h
m : Type ?u.2198697
n✝ : Type ?u.2198700
inst✝⁴ : DecidableEq n✝
inst✝³ : Fintype n✝
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
i : Fin (Nat.succ n)
this : det A = (-1) ^ ↑i * ↑↑(↑sign (Fin.cycleRange i)⁻¹) * det A
j : Fin (Nat.succ n)
x✝ : j ∈ univ
i' j' : Fin n
⊢ A (↑(Fin.cycleRange i)⁻¹ (Fin.succ i')) (↑(Fin.succAbove j) j') = A (↑(Fin.succAbove i) i') (↑(Fin.succAbove j) j')
rw [Equiv.Perm.inv_def, Fin.cycleRange_symm_succ]