structure definition def or abbrev

`Projector`

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

formal statement (Lean)

  19structure Projector (H : Type*) [RSHilbertSpace H] extends Observable H where
  20  /-- Idempotent property -/
  21  idempotent : op.comp op = op
  22
  23/-- Hamiltonian operator -/

used by (1)

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

commutation_from_ledger in IndisputableMonolith.Quantum.CommutationStructure decl_use

depends on (11)

Lean names referenced from this declaration's body.

comp in IndisputableMonolith.Algebra.CostAlgebra decl_use
H in IndisputableMonolith.Algebra.CostAlgebra decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
comp in IndisputableMonolith.Foundation.ArithmeticOf decl_use
Observable in IndisputableMonolith.Foundation.RecognitionForcing decl_use
Observable in IndisputableMonolith.Measurement.RSNative.Core decl_use
RSHilbertSpace in IndisputableMonolith.Quantum.HilbertSpace decl_use
Hamiltonian in IndisputableMonolith.Quantum.Observables decl_use
Observable in IndisputableMonolith.Quantum.Observables decl_use
comp in IndisputableMonolith.RRF.Core.Octave decl_use
comp in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use