lemma proved term proof

`two_mul_alphaLock`

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

formal statement (Lean)

 224lemma two_mul_alphaLock : 2 * alphaLock = 1 - 1 / phi := by

Term-mode proof.

 225  unfold alphaLock
 226  ring_nf
 227

Lean names referenced from this declaration's body.