recognition / Constants / Constants.Codata / hbar_pos

lemma

`hbar_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants.Codata
domain: Constants
line: 36 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.Codata on GitHub at line 36.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

Derivations using this theorem

Explicit CODATA Handles in the Canon · applied / MODEL
The canon ships concrete definitions of c, hbar, G as CODATA constants for cross-checks

depends on

used by

formal source

  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

papers checked against this theorem

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