add_mem_Radical

formal source

  39  unfold Radical dot
  40  simp
  41
  42theorem add_mem_Radical {n : ℕ} (α : Vec n) {v w : Vec n}
  43    (hv : v ∈ Radical α) (hw : w ∈ Radical α) :
  44    v + w ∈ Radical α := by
  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
  54theorem smul_mem_Radical {n : ℕ} (α : Vec n) {v : Vec n} (s : ℝ)
  55    (hv : v ∈ Radical α) :
  56    s • v ∈ Radical α := by
  57  unfold Radical dot at hv ⊢
  58  calc
  59    ∑ i : Fin n, α i * (s * v i)
  60        = s * ∑ i : Fin n, α i * v i := by
  61            rw [Finset.mul_sum]
  62            apply Finset.sum_congr rfl
  63            intro i hi
  64            ring
  65    _ = 0 := by rw [hv]; ring
  66
  67theorem sub_mem_Radical {n : ℕ} (α : Vec n) {v w : Vec n}
  68    (hv : v ∈ Radical α) (hw : w ∈ Radical α) :
  69    v - w ∈ Radical α := by
  70  simpa [sub_eq_add_neg] using
  71    add_mem_Radical α hv (smul_mem_Radical α (-1) hw)
  72