theorem proved term proof

`complex_hilbert_structure`

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

formal statement (Lean)

  17theorem complex_hilbert_structure : complex_hilbert_from_ledger := by

proof body

Term-mode proof.

  18  intro H hH ψ
  19  exact ψ.norm_one
  20
  21/-- Universe-stable extractor for complex-Hilbert structure. -/
  22theorem complex_hilbert_implies_unit_norm.{u}
  23    (h : @complex_hilbert_from_ledger.{u}) : @complex_hilbert_from_ledger.{u} :=
  24  h
  25
  26end ComplexHilbertStructure
  27end Quantum
  28end 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
complex_hilbert_from_ledger in IndisputableMonolith.Quantum.ComplexHilbertStructure decl_use