def definition def or abbrev

`optimalBondCosine`

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

formal statement (Lean)

  63def optimalBondCosine (n : ℕ) : ℝ :=

Definition body.

  64  if n ≤ 1 then 0 else -1 / (n - 1 : ℝ)
  65
  66/-- Linear geometry (n=2) has angle = 180° (cos = -1). -/

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

linear_cosine in IndisputableMonolith.Chemistry.BondAngles decl_use
octahedral_formula_cosine in IndisputableMonolith.Chemistry.BondAngles decl_use
tetrahedral_cosine in IndisputableMonolith.Chemistry.BondAngles decl_use
trigonal_cosine in IndisputableMonolith.Chemistry.BondAngles decl_use

Lean names referenced from this declaration's body.