def definition def or abbrev

`qfoCert`

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

formal statement (Lean)

  39def qfoCert : QFOCert where
  40  five_fields := quantumFieldTypeCount

Definition body.

  41  ten_total := statistics_times_fields
  42
  43end IndisputableMonolith.Physics.QuantumFieldOperatorsFromRS

Lean names referenced from this declaration's body.

QFOCert in IndisputableMonolith.Physics.QuantumFieldOperatorsFromRS decl_use
quantumFieldTypeCount in IndisputableMonolith.Physics.QuantumFieldOperatorsFromRS decl_use
statistics_times_fields in IndisputableMonolith.Physics.QuantumFieldOperatorsFromRS decl_use