Documentation

Lean 4 Proof

theorem cycle_product_scales_with_J {N : ℕ} (alpha : ℝ) (k : Fin N → ℝ) :
    (∏ n : Fin N, alpha * k n) = alpha ^ N * ∏ n : Fin N, k n := by
  rw [Finset.prod_mul_distrib, Finset.prod_const, Finset.card_univ, Fintype.card_fin]

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/HierarchicalJ.lean:44

Module Section

Paper 3c, Section 6: Hierarchical Implications

In the same file