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

layerSysPlus_comp

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)

 743def layerSysPlus_comp {n : ℕ} {A B C : LayerSysPlusObj n}
 744    (g : LayerSysPlusHom B C) (f : LayerSysPlusHom A B) : LayerSysPlusHom A C where
 745  costHom := recAlg_comp g.costHom f.costHom

proof body

Definition body.

 746  phiHom := phiRing_comp g.phiHom f.phiHom
 747  ledgerHom := ledgerAlg_comp g.ledgerHom f.ledgerHom
 748  octaveHom := octaveAlg_comp g.octaveHom f.octaveHom
 749
 750/-- The canonical linked system built from the verified cost, `φ`, ledger, and
 751    octave layers. -/

depends on (21)

Lean names referenced from this declaration's body.