theorem
proved
tactic proof
add_mem_Radical
show as:
view Lean formalization →
formal statement (Lean)
42theorem add_mem_Radical {n : ℕ} (α : Vec n) {v w : Vec n}
43 (hv : v ∈ Radical α) (hw : w ∈ Radical α) :
44 v + w ∈ Radical α := by
proof body
Tactic-mode proof.
45 unfold Radical dot at hv hw ⊢
46 have hv0 : ∑ i : Fin n, α i * v i = 0 := hv
47 have hw0 : ∑ i : Fin n, α i * w i = 0 := hw
48 calc
49 ∑ i : Fin n, α i * (v i + w i)
50 = (∑ i : Fin n, α i * v i) + ∑ i : Fin n, α i * w i := by
51 simp [mul_add, Finset.sum_add_distrib]
52 _ = 0 := by rw [hv0, hw0]; ring
53