118noncomputable def ofMicroMoves (moves : List MicroMove) : NormalForm where 119 supportPairs := (moves.map (·.pair)).toFinset.filter (fun k =>
proof body
Definition body.
120 ∃ prim, aggCoeff moves k prim ≠ 0) 121 coeff := aggCoeff moves 122 zero_outside := ofMicroMoves_zero_outside moves 123 nontrivial := ofMicroMoves_nontrivial moves 124 125/-- Every micro-move generated for `pair` stays within that pair scope. 126 127Proof: rowMoves constructs MicroMove.mk with pair as first argument, 128so any move in the list has m.pair = pair by construction. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.