structure definition def or abbrev

`SuperconductorVortexCert`

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

formal statement (Lean)

  33structure SuperconductorVortexCert where
  34  five_lattice_types : Fintype.card VortexLatticeType = 5
  35  flux_quantum_cost : Jcost 1 = 0
  36

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

superconductorVortexCert in IndisputableMonolith.Materials.SuperconductorVortexFromJCost decl_use

Lean names referenced from this declaration's body.

VortexLatticeType in IndisputableMonolith.Materials.SuperconductorVortexFromJCost decl_use