def definition def or abbrev

`shellCapacity`

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

formal statement (Lean)

 106def shellCapacity (n : ℕ) : ℕ := 2 * n^2

Definition body.

 107
 108/-- **THEOREM**: First shell (n=1) holds 2 electrons. -/

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

shellCapacity in IndisputableMonolith.Chemistry.PeriodicTable decl_use
PeriodicTableCert in IndisputableMonolith.Chemistry.PeriodicTableFromPhiLadder decl_use
shellCapacity in IndisputableMonolith.Chemistry.PeriodicTableFromPhiLadder decl_use
shellCapacity_1 in IndisputableMonolith.Chemistry.PeriodicTableFromPhiLadder decl_use
shellCapacity_2 in IndisputableMonolith.Chemistry.PeriodicTableFromPhiLadder decl_use
shellCapacity_3 in IndisputableMonolith.Chemistry.PeriodicTableFromPhiLadder decl_use
shellCapacity_4 in IndisputableMonolith.Chemistry.PeriodicTableFromPhiLadder decl_use
first_shell_capacity in IndisputableMonolith.QFT.PauliExclusion decl_use
fourth_shell_capacity in IndisputableMonolith.QFT.PauliExclusion decl_use
second_shell_capacity in IndisputableMonolith.QFT.PauliExclusion decl_use
shell_filling_pattern in IndisputableMonolith.QFT.PauliExclusion decl_use
third_shell_capacity in IndisputableMonolith.QFT.PauliExclusion decl_use

Lean names referenced from this declaration's body.

shell in IndisputableMonolith.Chemistry.PeriodicBlocks decl_use
shellCapacity in IndisputableMonolith.Chemistry.PeriodicTable decl_use
shellCapacity in IndisputableMonolith.Chemistry.PeriodicTableFromPhiLadder decl_use