theorem proved term proof

`cube_face_equicardinal`

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

formal statement (Lean)

  69theorem cube_face_equicardinal
  70    {A B : Type} [Fintype A] [Fintype B]
  71    (hA : HasCubeFaceCount A) (hB : HasCubeFaceCount B) :
  72    Fintype.card A = Fintype.card B := by

proof body

Term-mode proof.

  73  rw [hA, hB]
  74
  75/-- Standard Model total fermion count: 6 quarks + 6 leptons = 12. -/

depends on (7)

Lean names referenced from this declaration's body.

Model in IndisputableMonolith.CPM.LawOfExistence decl_use
HasCubeFaceCount in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
total in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use