Theorem: MatrixCookbook.eq_24 (MatrixCookbook/1Basic.lean)

State before:
ι : Type ?u.26561
R : Type u_1
m : Type u_2
n : Type ?u.26570
p : Type ?u.26573
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : Field R
u v : m → R
⊢ (1 + col u * row v).det = 1 + u ⬝ᵥ v
Tactic:
rw [det_one_add_col_mul_row u v, dotProduct_comm]
State after:
no goals