theorem
proved
tactic proof
AApply_sq
show as:
view Lean formalization →
formal statement (Lean)
119theorem AApply_sq {n : ℕ}
120 (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β v : Vec n) :
121 AApply lam hInv β (AApply lam hInv β v) = mu lam hInv β • AApply lam hInv β v := by
proof body
Tactic-mode proof.
122 funext i
123 have hdot :
124 dot β (fun k => lam * sharp hInv β k * dot β v) = mu lam hInv β * dot β v := by
125 simpa [AApply] using dot_AApply lam hInv β v
126 unfold AApply
127 rw [hdot]
128 simp [mu]
129 ring
130