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 α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ ↑(RingHom.mapMatrix f) (adjugate M) i k = adjugate (↑(RingHom.mapMatrix f) M) i k
m : Type u
n : Type v
α : Type w
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : CommRing α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
⊢ ↑(RingHom.mapMatrix f) (adjugate M) = adjugate (↑(RingHom.mapMatrix f) M)
ext (i k)
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 α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ↑f ∘ Pi.single i 1
⊢ ↑(RingHom.mapMatrix f) (adjugate M) i k = adjugate (↑(RingHom.mapMatrix f) M) i k
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 α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ ↑(RingHom.mapMatrix f) (adjugate M) i k = adjugate (↑(RingHom.mapMatrix f) M) i k
have : Pi.single i (1 : S) = f ∘ Pi.single i 1 := by
  rw [← f.map_one]
  exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)
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 α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ↑f ∘ Pi.single i 1
⊢ ↑(RingHom.mapMatrix f) (adjugate M) i k = adjugate (↑(RingHom.mapMatrix f) M) i k
rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←
  map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]
m : Type u
n : Type v
α : Type w
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : CommRing α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i (↑f 1) = ↑f ∘ Pi.single i 1
m : Type u
n : Type v
α : Type w
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : CommRing α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i 1 = ↑f ∘ Pi.single i 1
rw [← f.map_one]
no goals
m : Type u
n : Type v
α : Type w
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : CommRing α
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
⊢ Pi.single i (↑f 1) = ↑f ∘ Pi.single i 1
exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)