pith. machine review for the scientific record. sign in
structure definition def or abbrev

LatticeMeasure

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  11structure LatticeMeasure where
  12  deriving Inhabited
  13
  14/-- Transfer kernel acting on complex observables. -/

used by (9)

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

depends on (2)

Lean names referenced from this declaration's body.