`c_SI`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.ExternalAnchors
domain: Constants
line: 67 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.ExternalAnchors on GitHub at line 67.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  64
  65/-- **EXTERNAL ANCHOR**: Speed of light in vacuum (exact, SI 2019 definition).
  66    c = 299792458 m/s -/
  67@[simp]
  68noncomputable def c_SI : ℝ := 299792458
  69
  70/-- **EXTERNAL ANCHOR**: Reduced Planck constant (exact, SI 2019 definition).
  71    ℏ = 1.054571817... × 10⁻³⁴ J·s -/
  72@[simp]
  73noncomputable def hbar_SI : ℝ := 1.054571817e-34
  74
  75/-- **EXTERNAL ANCHOR**: Planck constant (exact, SI 2019 definition).
  76    h = 6.62607015 × 10⁻³⁴ J·s -/
  77@[simp]
  78noncomputable def h_SI : ℝ := 6.62607015e-34
  79
  80/-- **EXTERNAL ANCHOR**: Elementary charge (exact, SI 2019 definition).
  81    e = 1.602176634 × 10⁻¹⁹ C -/
  82@[simp]
  83noncomputable def e_SI : ℝ := 1.602176634e-19
  84
  85/-- **EXTERNAL ANCHOR**: Boltzmann constant (exact, SI 2019 definition).
  86    k_B = 1.380649 × 10⁻²³ J/K -/
  87@[simp]
  88noncomputable def kB_SI : ℝ := 1.380649e-23
  89
  90/-- **EXTERNAL ANCHOR**: Avogadro constant (exact, SI 2019 definition).
  91    N_A = 6.02214076 × 10²³ mol⁻¹ -/
  92@[simp]
  93noncomputable def NA_SI : ℝ := 6.02214076e23
  94
  95/-- **EXTERNAL ANCHOR**: Gravitational constant (CODATA 2022, measured).
  96    G = 6.67430(15) × 10⁻¹¹ m³/(kg·s²)
  97    Relative uncertainty: 2.2 × 10⁻⁵ -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.