inductive definition def or abbrev

`MagnetismType`

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

formal statement (Lean)

  16inductive MagnetismType where
  17  | diamagnetism
  18  | paramagnetism
  19  | ferromagnetism
  20  | antiferromagnetism
  21  | ferrimagnetism
  22  deriving DecidableEq, Repr, BEq, Fintype
  23

used by (2)

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

magnetismType_count in IndisputableMonolith.Materials.MagnetismTypesFromConfigDim decl_use
MagnetismTypesCert in IndisputableMonolith.Materials.MagnetismTypesFromConfigDim decl_use