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 α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
hAB : IsLeftRegular (det (A ⬝ B))
⊢ 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 α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
have hAB : IsLeftRegular (A ⬝ B).det := by
  rw [det_mul]
  exact hA.mul hB
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 α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
hAB : IsLeftRegular (det (A ⬝ B))
⊢ (fun x => A ⬝ B * x) (adjugate (A ⬝ B)) = (fun x => A ⬝ B * x) (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 α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
hAB : IsLeftRegular (det (A ⬝ B))
⊢ adjugate (A ⬝ B) = adjugate B ⬝ adjugate A
refine' (isRegular_of_isLeftRegular_det hAB).left _
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 α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
hAB : IsLeftRegular (det (A ⬝ B))
⊢ A ⬝ B * adjugate (A ⬝ B) = 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 α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
hAB : IsLeftRegular (det (A ⬝ B))
⊢ (fun x => A ⬝ B * x) (adjugate (A ⬝ B)) = (fun x => A ⬝ B * x) (adjugate B ⬝ adjugate A)
simp only
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 α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
hAB : IsLeftRegular (det (A ⬝ B))
⊢ A ⬝ B * adjugate (A ⬝ B) = A ⬝ B * adjugate B ⬝ adjugate A
rw [mul_eq_mul, mul_adjugate, mul_eq_mul, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
  smul_mul, Matrix.one_mul, mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_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 α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
⊢ IsLeftRegular (det A * det B)
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 α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
⊢ IsLeftRegular (det (A ⬝ B))
rw [det_mul]
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 α
hA : IsLeftRegular (det A)
hB : IsLeftRegular (det B)
⊢ IsLeftRegular (det A * det B)
exact hA.mul hB