pith. machine review for the scientific record. sign in
lemma proved term proof

mem_toMoves_of_coeff_ne_zero

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)

 420lemma mem_toMoves_of_coeff_ne_zero (nf : NormalForm) {pair : ℕ} {prim : Primitive}
 421    (hsupp : pair ∈ nf.supportPairs) (hcoeff : nf.coeff pair prim ≠ 0) :
 422    ⟨pair, prim, nf.coeff pair prim⟩ ∈ toMoves nf := by

proof body

Term-mode proof.

 423  classical
 424  unfold toMoves
 425  have hpair : pair ∈ pairList nf := (pairList_mem).2 hsupp
 426  exact List.mem_flatMap.mpr
 427    ⟨pair, hpair, rowMoves_mem_of_coeff_ne_zero (nf := nf) (pair := pair) (prim := prim) hcoeff⟩
 428
 429/-- The mapped pair list produced by `toMoves` contains any supported pair with non-zero coeff. -/

used by (1)

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

depends on (10)

Lean names referenced from this declaration's body.