theorem proved term proof

`card_eq`

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

formal statement (Lean)

 121theorem card_eq : Fintype.card (F2Power D) = 2 ^ D := by

Term-mode proof.

 122  unfold F2Power
 123  simp [Fintype.card_bool, Fintype.card_fin]
 124
 125/-- The number of non-zero vectors in `F2Power D` is `2 ^ D - 1`. -/

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

Lean names referenced from this declaration's body.

F2Power in IndisputableMonolith.Algebra.F2Power decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use