theorem proved term proof

`commutation_structure`

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

formal statement (Lean)

  12theorem commutation_structure : commutation_from_ledger := by

proof body

Term-mode proof.

  13  intro H hH P
  14  exact P.idempotent
  15
  16/-- Universe-stable extractor for commutation structure. -/
  17theorem commutation_implies_projector_idempotent.{u}
  18    (h : @commutation_from_ledger.{u}) : @commutation_from_ledger.{u} :=
  19  h
  20
  21end CommutationStructure
  22end Quantum
  23end IndisputableMonolith

depends on (4)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
commutation_from_ledger in IndisputableMonolith.Quantum.CommutationStructure decl_use