def definition def or abbrev

`plotWeight`

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

formal statement (Lean)

 253def plotWeight (p : BookerPlotFamily) : ℕ :=

proof body

Definition body.

 254  F2Power.hammingWeight (plotEncoding p)
 255
 256/-- The three single-axis plots (primary): Rags to Riches, Voyage and
 257    Return, Comedy. -/

used by (3)

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

singleAxis_plots in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
threeAxis_plots in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
twoAxis_plots in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use

depends on (5)

Lean names referenced from this declaration's body.

BookerPlotFamily in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
plotEncoding in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
F2Power in IndisputableMonolith.Algebra.F2Power decl_use
hammingWeight in IndisputableMonolith.Algebra.F2Power decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use