def definition def or abbrev

`hammingWeight`

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

formal statement (Lean)

 152def hammingWeight (v : F2Power D) : ℕ :=

Definition body.

 153  (Finset.univ.filter (fun i => v i = true)).card
 154

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

plotWeight in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
singleAxis_plots in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
threeAxis_plots in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
twoAxis_plots in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
axis123_weight in IndisputableMonolith.Algebra.F2Power decl_use
axis1_weight in IndisputableMonolith.Algebra.F2Power decl_use
axis2_weight in IndisputableMonolith.Algebra.F2Power decl_use
axis3_weight in IndisputableMonolith.Algebra.F2Power decl_use
card_weight_zero_three in IndisputableMonolith.Algebra.F2Power decl_use
hammingWeight_le in IndisputableMonolith.Algebra.F2Power decl_use
hammingWeight_zero in IndisputableMonolith.Algebra.F2Power decl_use
weight_zero_iff in IndisputableMonolith.Algebra.F2Power decl_use

Lean names referenced from this declaration's body.