inductive definition def or abbrev

`InflationModel`

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

formal statement (Lean)

  18inductive InflationModel where
  19  | chaoticQuadratic
  20  | newInflationPlateau
  21  | hybrid
  22  | naturalAxionLike
  23  | alphaAttractor
  24  deriving DecidableEq, Repr, BEq, Fintype
  25

used by (8)

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

CosmicInflationCert in IndisputableMonolith.Cosmology.CosmicInflationFromJCost decl_use
InflationModel in IndisputableMonolith.Cosmology.CosmicInflationFromJCost decl_use
inflationModelCount in IndisputableMonolith.Cosmology.CosmicInflationFromJCost decl_use
inflationModel_count in IndisputableMonolith.Cosmology.InflationModelsFromConfigDim decl_use
InflationModelsCert in IndisputableMonolith.Cosmology.InflationModelsFromConfigDim decl_use
InflationaryCosm in IndisputableMonolith.Physics.InflationaryCosmologyFromRS decl_use
InflationModel in IndisputableMonolith.Physics.InflationaryCosmologyFromRS decl_use
inflationModelCount in IndisputableMonolith.Physics.InflationaryCosmologyFromRS decl_use

depends on (2)

Lean names referenced from this declaration's body.

InflationModel in IndisputableMonolith.Cosmology.CosmicInflationFromJCost decl_use
InflationModel in IndisputableMonolith.Physics.InflationaryCosmologyFromRS decl_use