theorem proved tactic proof

`nonzero_card_three`

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

formal statement (Lean)

 140theorem nonzero_card_three :
 141    (Finset.univ.filter (fun v : F2Power 3 => v ≠ 0)).card = 7 := by

proof body

Tactic-mode proof.

 142  have h := @nonzero_card 3
 143  -- h : … = 2 ^ 3 - 1
 144  have h2 : (2 : ℕ) ^ 3 - 1 = 7 := by norm_num
 145  rw [h2] at h
 146  exact h
 147
 148/-! ## Hamming weight -/
 149
 150/-- The Hamming weight of `v`: the number of coordinates equal to
 151    `true`. -/

used by (2)

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

plotEncoding_image_eq_nonzero in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
Q3_nontrivial_subgroup_count in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use

depends on (7)

Lean names referenced from this declaration's body.

F2Power in IndisputableMonolith.Algebra.F2Power decl_use
nonzero_card in IndisputableMonolith.Algebra.F2Power decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use