`add`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.Ledger
domain: RRF
line: 50 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RRF.Foundation.Ledger on GitHub at line 50.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  47def zero : Transaction := fromAmount 0
  48
  49/-- Transactions form an additive structure. -/
  50def add (t₁ t₂ : Transaction) : Transaction := {
  51  debit := t₁.debit + t₂.debit,
  52  credit := t₁.credit + t₂.credit,
  53  balanced := by
  54    have h₁ := t₁.balanced
  55    have h₂ := t₂.balanced
  56    omega
  57}
  58
  59theorem add_balanced (t₁ t₂ : Transaction) :
  60    (add t₁ t₂).debit + (add t₁ t₂).credit = 0 := (add t₁ t₂).balanced
  61
  62end Transaction
  63
  64/-! ## Full Ledger -/
  65
  66/-- A ledger: a sequence of transactions that globally balance. -/
  67structure Ledger where
  68  /-- The transactions in the ledger. -/
  69  transactions : List Transaction
  70  /-- Total debit. -/
  71  total_debit : ℤ := (transactions.map (·.debit)).sum
  72  /-- Total credit. -/
  73  total_credit : ℤ := (transactions.map (·.credit)).sum
  74  /-- Global balance: total debit + total credit = 0. -/
  75  global_balance : total_debit + total_credit = 0
  76
  77namespace Ledger
  78
  79/-- The empty ledger. -/
  80def empty : Ledger := {

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.