theorem
proved
tactic proof
dot_AApply
show as:
view Lean formalization →
formal statement (Lean)
103theorem dot_AApply {n : ℕ}
104 (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β v : Vec n) :
105 dot β (AApply lam hInv β v) = mu lam hInv β * dot β v := by
proof body
Tactic-mode proof.
106 unfold dot AApply mu
107 calc
108 ∑ i : Fin n, β i * (lam * sharp hInv β i * dot β v)
109 = (lam * dot β v) * ∑ i : Fin n, β i * sharp hInv β i := by
110 rw [Finset.mul_sum]
111 apply Finset.sum_congr rfl
112 intro i hi
113 ring
114 _ = (lam * ∑ i : Fin n, β i * sharp hInv β i) * dot β v := by
115 ring
116 _ = mu lam hInv β * dot β v := by
117 simp [mu, dot]
118