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

LedgerAlgebra

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)

 201structure LedgerAlgebra where
 202  /-- The transaction type. -/
 203  transaction : Type := Transaction

proof body

Definition body.

 204  /-- The ledger type. -/
 205  ledger : Type := Ledger
 206  /-- Transactions are balanced. -/
 207  transactions_balanced : ∀ t : Transaction, t.debit + t.credit = 0 := fun t => t.balanced
 208  /-- Ledgers are balanced. -/
 209  ledgers_balanced : ∀ L : Ledger, L.net = 0 := fun L => L.global_balance
 210  /-- Double-entry holds. -/
 211  double_entry : DoubleEntry := double_entry_exists
 212
 213/-- The ledger algebra is consistent. -/

used by (4)

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

depends on (13)

Lean names referenced from this declaration's body.