def
definition
c
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Constants.Codata on GitHub at line 27.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
formal source
24/-! ## CODATA 2018 reference values -/
25
26/-- Speed of light (exact SI definition). -/
27@[simp] noncomputable def c : ℝ := 299792458
28
29/-- Reduced Planck constant (CODATA 2018). -/
30@[simp] noncomputable def hbar : ℝ := 1.054571817e-34
31
32/-- Gravitational constant (CODATA 2018). -/
33@[simp] noncomputable def G : ℝ := 6.67430e-11
34
35lemma c_pos : 0 < c := by unfold c; norm_num
36lemma hbar_pos : 0 < hbar := by unfold hbar; norm_num
37lemma G_pos : 0 < G := by unfold G; norm_num
38
39lemma c_ne_zero : c ≠ 0 := ne_of_gt c_pos
40lemma hbar_ne_zero : hbar ≠ 0 := ne_of_gt hbar_pos
41lemma G_ne_zero : G ≠ 0 := ne_of_gt G_pos
42
43end
44
45end Constants
46end IndisputableMonolith