structure definition def or abbrev

`NormalizedState`

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

formal statement (Lean)

  21structure NormalizedState (H : Type*) [RSHilbertSpace H] where
  22  vec : H
  23  norm_one : ‖vec‖ = 1
  24
  25end IndisputableMonolith.Quantum

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

complex_hilbert_from_ledger in IndisputableMonolith.Quantum.ComplexHilbertStructure decl_use
normalized_state_unit_norm in IndisputableMonolith.Quantum.ComplexHilbertStructure decl_use
Hamiltonian in IndisputableMonolith.Quantum.Observables decl_use
Substrate in IndisputableMonolith.Relativity.ILG.Substrate decl_use

Lean names referenced from this declaration's body.