abbrev definition def or abbrev

`MeasurementAngle`

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

formal statement (Lean)

  44abbrev MeasurementAngle := ℝ

Definition body.

  45
  46/-- A measurement outcome (+1 or -1). -/

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

chshCombination in IndisputableMonolith.Quantum.BellInequality decl_use
perfect_anticorrelation in IndisputableMonolith.Quantum.BellInequality decl_use
quantumCorrelation in IndisputableMonolith.Quantum.BellInequality decl_use
quantum_correlation_bounded in IndisputableMonolith.Quantum.BellInequality decl_use

Lean names referenced from this declaration's body.