structure definition def or abbrev

`NuclearMagicCert`

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

formal statement (Lean)

  38structure NuclearMagicCert where
  39  seven_magic : magicNumbers.card = 7
  40  eight_from_8tick : (8 : ℕ) = 2 ^ 3
  41  has_8 : 8 ∈ magicNumbers
  42  has_2 : 2 ∈ magicNumbers
  43

used by (3)

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

nuclearMagicCert in IndisputableMonolith.Chemistry.NuclearMagicIsotopesFromRS decl_use
NuclearMagicCert in IndisputableMonolith.Chemistry.NuclearMagicIsotopesFromRS decl_use
nuclearMagicCert in IndisputableMonolith.Physics.NuclearMagicNumbersFromRS decl_use

depends on (2)

Lean names referenced from this declaration's body.

NuclearMagicCert in IndisputableMonolith.Chemistry.NuclearMagicIsotopesFromRS decl_use
magicNumbers in IndisputableMonolith.Physics.NuclearMagicNumbersFromRS decl_use