m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
r : α
A : Matrix n n α
⊢ (↑of fun i => ↑(r ^ (Fintype.card n - 1) • cramer Aᵀ) (Pi.single i 1)) =
    r ^ (Fintype.card n - 1) • ↑of fun i => ↑(cramer Aᵀ) (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 : α
A : Matrix n n α
⊢ adjugate (r • A) = r ^ (Fintype.card n - 1) • adjugate A
rw [adjugate, adjugate, transpose_smul, cramer_smul]
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 : α
A : Matrix n n α
⊢ (↑of fun i => ↑(r ^ (Fintype.card n - 1) • cramer Aᵀ) (Pi.single i 1)) =
    r ^ (Fintype.card n - 1) • ↑of fun i => ↑(cramer Aᵀ) (Pi.single i 1)
rfl