R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ : Matrix n n R
M : Matrix n n R[X]
r : R
⊢ det (↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M) = det (eval (↑(scalar n) r) (↑matPolyEquiv M))
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ : Matrix n n R
M : Matrix n n R[X]
r : R
⊢ eval r (det M) = det (eval (↑(scalar n) r) (↑matPolyEquiv M))
rw [Polynomial.eval, ← coe_eval₂RingHom, RingHom.map_det]
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ : Matrix n n R
M : Matrix n n R[X]
r : R
⊢ ↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M = eval (↑(scalar n) r) (↑matPolyEquiv M)
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ : Matrix n n R
M : Matrix n n R[X]
r : R
⊢ det (↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M) = det (eval (↑(scalar n) r) (↑matPolyEquiv M))
apply congr_arg det
case a.h
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ : Matrix n n R
M : Matrix n n R[X]
r : R
i✝ x✝ : n
⊢ ↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M i✝ x✝ = eval (↑(scalar n) r) (↑matPolyEquiv M) i✝ x✝
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ : Matrix n n R
M : Matrix n n R[X]
r : R
⊢ ↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M = eval (↑(scalar n) r) (↑matPolyEquiv M)
ext
case a.h
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ : Matrix n n R
M : Matrix n n R[X]
r : R
i✝ x✝ : n
⊢ eval (↑(scalar n) r) (↑matPolyEquiv M) i✝ x✝ = ↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M i✝ x✝
case a.h
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ : Matrix n n R
M : Matrix n n R[X]
r : R
i✝ x✝ : n
⊢ ↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M i✝ x✝ = eval (↑(scalar n) r) (↑matPolyEquiv M) i✝ x✝
symm
no goals
case a.h
R : Type u
inst✝³ : CommRing R
n G : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
α β : Type v
inst✝ : DecidableEq α
M✝ : Matrix n n R
M : Matrix n n R[X]
r : R
i✝ x✝ : n
⊢ eval (↑(scalar n) r) (↑matPolyEquiv M) i✝ x✝ = ↑(RingHom.mapMatrix (eval₂RingHom (RingHom.id R) r)) M i✝ x✝
exact matPolyEquiv_eval _ _ _ _