`complex_hilbert_structure`

proved

show as: view math explainer →

module: IndisputableMonolith.Quantum.ComplexHilbertStructure
domain: Quantum
line: 17 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Quantum.ComplexHilbertStructure on GitHub at line 17.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  14    (ψ : NormalizedState H) : ‖ψ.vec‖ = 1 :=
  15  ψ.norm_one
  16
  17theorem complex_hilbert_structure : complex_hilbert_from_ledger := by
  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

papers checked against this theorem

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