-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem det_adjugate (A : Matrix n n α) : (adjugate A).det = A.det ^ (Fintype.card n - 1)

Proof state:
case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n > 0
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
replace h_card := tsub_add_cancel_of_le h_card.nat_succ_le

Result:
case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Proof state:
case inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n = 0
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
haveI : IsEmpty n := Fintype.card_eq_zero_iff.mp h_card

Result:
case inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n = 0
this : IsEmpty n
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det ^ Fintype.card n = A'.det * A'.det ^ (Fintype.card n - 1)

Tactic:
rw [← pow_succ', h_card]

Result:
no goals

Proof state:
case inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n = 0
this : IsEmpty n
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
rw [h_card, Nat.zero_sub, pow_zero, adjugate_subsingleton, det_one]

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
rcases (Fintype.card n).eq_zero_or_pos with h_card | h_card

Result:
case inl
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n = 0
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n > 0
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Proof state:
case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
suffices A'.adjugate.det = A'.det ^ (Fintype.card n - 1) by
  rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←
    AlgHom.map_det, ← map_pow, this]

Result:
case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.adjugate.det = A'.det ^ (Fintype.card n - 1)

Proof state:
case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det * A'.adjugate.det = A'.det * A'.det ^ (Fintype.card n - 1)

Tactic:
calc
  A'.det * A'.adjugate.det = (A' * adjugate A').det := (det_mul _ _).symm
  _ = A'.det ^ Fintype.card n := by rw [mul_adjugate, det_smul, det_one, mul_one]
  _ = A'.det * A'.det ^ (Fintype.card n - 1) := by rw [← pow_succ', h_card]

Result:
no goals

Proof state:
case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
let A' := mvPolynomialX n n ℤ

Result:
case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ (A' * A'.adjugate).det = A'.det ^ Fintype.card n

Tactic:
rw [mul_adjugate, det_smul, det_one, mul_one]

Result:
no goals

Proof state:
case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.adjugate.det = A'.det ^ (Fintype.card n - 1)

Tactic:
apply mul_left_cancel₀ (show A'.det ≠ 0 from det_mvPolynomialX_ne_zero n ℤ)

Result:
case inr
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
⊢ A'.det * A'.adjugate.det = A'.det * A'.det ^ (Fintype.card n - 1)

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h_card : Fintype.card n - Nat.succ 0 + Nat.succ 0 = Fintype.card n
A' : Matrix n n (MvPolynomial (n × n) ℤ) := mvPolynomialX n n ℤ
this : A'.adjugate.det = A'.det ^ (Fintype.card n - 1)
⊢ A.adjugate.det = A.det ^ (Fintype.card n - 1)

Tactic:
rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←
  AlgHom.map_det, ← map_pow, this]

Result:
no goals