m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
let g : Matrix n n α → Matrix n n α[X] := fun M =>
  M.map Polynomial.C + (Polynomial.X : α[X]) • (1 : Matrix n n α[X])
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
let f' : Matrix n n α[X] →+* Matrix n n α := (Polynomial.evalRingHom 0).mapMatrix
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
have f'_inv : ∀ M, f' (g M) = M := by
  intro
  ext
  simp
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
have f'_adj : ∀ M : Matrix n n α, f' (adjugate (g M)) = adjugate M := by
  intro
  rw [RingHom.map_adjugate, f'_inv]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M ⬝ g N) = M ⬝ N
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
have f'_g_mul : ∀ M N : Matrix n n α, f' (g M ⬝ g N) = M ⬝ N := by
  intros M N
  rw [← mul_eq_mul, RingHom.map_mul, f'_inv, f'_inv, mul_eq_mul M N]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M ⬝ g N) = M ⬝ N
hu : ∀ (M : Matrix n n α), IsRegular (det (g M))
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M ⬝ g N) = M ⬝ N
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
have hu : ∀ M : Matrix n n α, IsRegular (g M).det := by
  intro M
  refine' Polynomial.Monic.isRegular _
  simp only [Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm]
no goals
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M ⬝ g N) = M ⬝ N
hu : ∀ (M : Matrix n n α), IsRegular (det (g M))
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
rw [← f'_adj, ← f'_adj, ← f'_adj, ← mul_eq_mul (f' (adjugate (g B))), ← f'.map_mul, mul_eq_mul, ←
  adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,
  RingHom.map_adjugate, f'_inv, f'_g_mul]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
M✝ : Matrix n n α
⊢ ↑f' (g M✝) = M✝
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
⊢ ∀ (M : Matrix n n α), ↑f' (g M) = M
intro
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
M✝ : Matrix n n α
i✝ x✝ : n
⊢ ↑f' (g M✝) i✝ x✝ = M✝ i✝ x✝
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
M✝ : Matrix n n α
⊢ ↑f' (g M✝) = M✝
ext
no goals
case a.h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
M✝ : Matrix n n α
i✝ x✝ : n
⊢ ↑f' (g M✝) i✝ x✝ = M✝ i✝ x✝
simp
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
M✝ : Matrix n n α
⊢ ↑f' (adjugate (g M✝)) = adjugate M✝
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
⊢ ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
intro
no goals
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
M✝ : Matrix n n α
⊢ ↑f' (adjugate (g M✝)) = adjugate M✝
rw [RingHom.map_adjugate, f'_inv]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
M N : Matrix n n α
⊢ ↑f' (g M ⬝ g N) = M ⬝ N
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
⊢ ∀ (M N : Matrix n n α), ↑f' (g M ⬝ g N) = M ⬝ N
intros M N
no goals
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
M N : Matrix n n α
⊢ ↑f' (g M ⬝ g N) = M ⬝ N
rw [← mul_eq_mul, RingHom.map_mul, f'_inv, f'_inv, mul_eq_mul M N]
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M ⬝ g N) = M ⬝ N
M : Matrix n n α
⊢ IsRegular (det (g M))
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M ⬝ g N) = M ⬝ N
⊢ ∀ (M : Matrix n n α), IsRegular (det (g M))
intro M
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M ⬝ g N) = M ⬝ N
M : Matrix n n α
⊢ Monic (det (g M))
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M ⬝ g N) = M ⬝ N
M : Matrix n n α
⊢ IsRegular (det (g M))
refine' Polynomial.Monic.isRegular _
no goals
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A B : Matrix n n α
g : Matrix n n α → Matrix n n α[X] := fun M => map M ↑C + X • 1
f' : Matrix n n α[X] →+* Matrix n n α := RingHom.mapMatrix (evalRingHom 0)
f'_inv : ∀ (M : Matrix n n α), ↑f' (g M) = M
f'_adj : ∀ (M : Matrix n n α), ↑f' (adjugate (g M)) = adjugate M
f'_g_mul : ∀ (M N : Matrix n n α), ↑f' (g M ⬝ g N) = M ⬝ N
M : Matrix n n α
⊢ Monic (det (g M))
simp only [Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm]