pith. machine review for the scientific record. sign in
def definition def or abbrev

aggCoeff

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)

  80noncomputable def aggCoeff (moves : List MicroMove) (pair : ℕ) (prim : Primitive) : ℝ :=

proof body

Definition body.

  81  ((moves.filter fun m => m.pair = pair ∧ m.primitive = prim).map (·.coeff)).sum
  82
  83/-- **NormalForm construction**: The ofMicroMoves construction is well-formed.
  84
  85Proof by contraposition: if aggCoeff is nonzero, pair must be in the filtered set.
  86-/

used by (9)

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

depends on (11)

Lean names referenced from this declaration's body.