Documentation

Lean 4 Proof

theorem shareFunction_scale_invariant {w : Fin J → ℝ}
    {c : ℝ} (hc : c ≠ 0) (j : Fin J) :
    shareFunction (fun k => c * w k) j = shareFunction w j := by
  simp only [shareFunction, ← Finset.mul_sum]
  exact mul_div_mul_left (w j) (∑ k, w k) hc

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:106

Module Section

Ten Views of a Single Object:

In the same file