theorem
proved
term proof
linear_cosine
show as:
view Lean formalization →
formal statement (Lean)
67theorem linear_cosine : optimalBondCosine 2 = -1 := by
proof body
Term-mode proof.
68 simp only [optimalBondCosine]
69 norm_num
70
71/-- Trigonal planar (n=3) has angle ≈ 120° (cos = -1/2). -/