Documentation

Lean 4 Proof

theorem shareFunction_sum_one {w : Fin J → ℝ}
    (hw : (∑ k : Fin J, w k) ≠ 0) :
    ∑ j : Fin J, shareFunction w j = 1 := by
  simp only [shareFunction, ← Finset.sum_div]
  exact div_self hw

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:66

Module Section

Ten Views of a Single Object:

In the same file