def definition def or abbrev

`concat`

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

formal statement (Lean)

 113def concat (L₁ L₂ : Ledger) : Ledger := {

proof body

Definition body.

 114  transactions := L₁.transactions ++ L₂.transactions,
 115  total_debit := L₁.total_debit + L₂.total_debit,
 116  total_credit := L₁.total_credit + L₂.total_credit,
 117  global_balance := by
 118    have h₁ := L₁.global_balance
 119    have h₂ := L₂.global_balance
 120    omega
 121}
 122

used by (1)

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

concat_preserves_balance in IndisputableMonolith.RRF.Foundation.Ledger decl_use