pith. machine review for the scientific record. sign in
theorem proved tactic proof

smul_mem_Radical

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  54theorem smul_mem_Radical {n : ℕ} (α : Vec n) {v : Vec n} (s : ℝ)
  55    (hv : v ∈ Radical α) :
  56    s • v ∈ Radical α := by

proof body

Tactic-mode proof.

  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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.