lemma proved term proof

`aggCoeff_append`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 368lemma aggCoeff_append (xs ys : List MicroMove) (pair : ℕ) (prim : Primitive) :
 369    aggCoeff (xs ++ ys) pair prim = aggCoeff xs pair prim + aggCoeff ys pair prim := by

proof body

Term-mode proof.

 370  classical
 371  unfold aggCoeff
 372  simp only [List.filter_append, List.map_append, List.sum_append]
 373
 374/-- Aggregation over a flat-mapped list of row moves. -/

used by (1)

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

aggCoeff_flatMap in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
aggCoeff in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
MicroMove in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
Primitive in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
Primitive in IndisputableMonolith.Masses.SectorPrimitive decl_use
row in IndisputableMonolith.YM.Dobrushin decl_use