IndisputableMonolith.Chemistry.PeriodicTable

declarations in this module (39)

• inductive Block L38
• class BlockOffsets L41
• def default L46
• def railFactor L61
• def blockFactor L66
• def railEnergy L71
• def window8Sum L75
• def nobleGasZ L85
• def nobleGasZFull L88
• def shellCapacity L94
• def cumulativeShellClosure L106
• def periodOf L116
• def prevClosure L126
• def nextClosure L136
• def distToNextClosure L147
• def valenceElectrons L152
• def periodLength L155
• def signedValenceCost L162
• def isNobleGas L168
• theorem helium_is_noble L177
• theorem neon_is_noble L180
• theorem argon_is_noble L183
• theorem krypton_is_noble L186
• theorem xenon_is_noble L189
• theorem radon_is_noble L192
• theorem noble_gas_at_closure L195
• theorem noble_gas_complete_shell L201
• theorem cumulative_closure_eq_noble L208
• theorem shell_sum_to_noble L213
• def periodLengths L221
• theorem period_lengths_from_noble_gaps L224
• def blockElectronCount L229
• theorem block_count_formula L236
• structure Index L247
• def indexOf L253
• def bandMultiplier L265
• def bandEnergy L271
• def neutralAt L276
• theorem neutralAt_const_zero L280