pith. machine review for the scientific record. sign in
def definition def or abbrev

yardstick

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 123@[simp] noncomputable def yardstick (s : Sector) : ℝ :=

proof body

Definition body.

 124  (2 : ℝ) ^ (B_pow s) * E_coh * Constants.phi ^ (r0 s)
 125
 126end Anchor
 127
 128namespace Integers
 129
 130/-- Generation torsion (global, representation-independent).
 131    τ(0) = 0, τ(1) = E_passive = 11, τ(2) = W = 17 -/

used by (20)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (20)

Lean names referenced from this declaration's body.