m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ map (adjugate A)ᵀ star = adjugate (map Aᵀ star)
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ (adjugate A)ᴴ = adjugate Aᴴ
dsimp only [conjTranspose]
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
this : map (adjugate Aᵀ) star = adjugate (map Aᵀ star)
⊢ map (adjugate A)ᵀ star = adjugate (map Aᵀ star)
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ map (adjugate A)ᵀ star = adjugate (map Aᵀ star)
have : Aᵀ.adjugate.map star = adjugate (Aᵀ.map star) := (starRingEnd α).map_adjugate Aᵀ
no goals
m : Type u
n : Type v
α : Type w
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
this : map (adjugate Aᵀ) star = adjugate (map Aᵀ star)
⊢ map (adjugate A)ᵀ star = adjugate (map Aᵀ star)
rw [A.adjugate_transpose, this]