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

dot_affineShift

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)

  90theorem dot_affineShift {n : ℕ} (α t v : Vec n) (s : ℝ) :
  91    dot α (affineShift t v s) = dot α t + s * dot α v := by

proof body

Tactic-mode proof.

  92  unfold dot affineShift
  93  calc
  94    ∑ i : Fin n, α i * (t i + s * v i)
  95        = ∑ i : Fin n, (α i * t i + s * (α i * v i)) := by
  96            apply Finset.sum_congr rfl
  97            intro i hi
  98            ring
  99    _ = (∑ i : Fin n, α i * t i) + s * ∑ i : Fin n, α i * v i := by
 100          rw [Finset.sum_add_distrib, Finset.mul_sum]
 101
 102/-- Directions in the radical stay inside the affine leaves `dot α = c`. -/

used by (2)

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

depends on (4)

Lean names referenced from this declaration's body.