PhysLean Documentation

PhysLean.StatisticalMechanics.BoltzmannConstant

Boltzmann constant #

The Boltzmann constant is a constant kB of dimension m² kg s⁻² K⁻¹, that is Energy/Temperature. It is named after Ludwig Boltzmann.

In this module give the value of the Boltzmann constant.

source
def Constants.kBAx :
↑{p : ℝ | 0 < p}

The Boltzmann constant in units of m ^ 2 kg s ^ (-2) K ^ (-1). As long as one does not use the underlying value of this quantity, then it can be used as Boltzmann's constant in an arbitrary set of units.

Equations
Instances For
    source
    noncomputable def Constants.kB :
    ℝ

    The Boltzmann constant in a given but arbitrary set of units. Boltzman's constant has dimension equivalent to Energy/Temperature.

    Equations
    Instances For
      source
      theorem Constants.kB_pos :
      0 < kB

      The Boltzmann constant is positive.

      source
      theorem Constants.kB_nonneg :
      0 ≤ kB

      The Boltzmann constant is non-negative.

      source
      theorem Constants.kB_ne_zero :
      kB ≠ 0

      The Boltzmann constant is not equal to zero.