pith. machine review for the scientific record. sign in
theorem proved tactic proof

row_anchor_bottom_strange_ratio_exp

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)

 103theorem row_anchor_bottom_strange_ratio_exp :
 104    massAtAnchor .b / massAtAnchor .s =
 105      Real.exp ((6 : ℝ) * Real.log phi) := by

proof body

Tactic-mode proof.

 106  have hZ : ZOf .b = ZOf .s := by decide
 107  have h := anchor_ratio .b .s hZ
 108  have hr : ((rung .b : ℝ) - rung .s) = (6 : ℝ) := by
 109    simp [rung]
 110    norm_num
 111  simpa [hr] using h
 112

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.