Documentation

Lean 4 Proof

def cycleProduct_real (N : ℕ) (k : Fin N → ℝ) : ℝ :=
  ∏ n : Fin N, k n

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:130

Module Section

## Entry-Exit Core Definitions (merged from EntryExitDefs.lean)

In the same file