def definition def or abbrev

`circumscribedPerimeter`

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

formal statement (Lean)

  82noncomputable def circumscribedPerimeter (n : ℕ) (hn : n ≥ 3) : ℝ :=

proof body

Definition body.

  83  n * 2 * Real.tan (π / n)
  84
  85/-- For 8-gon (octagon):
  86    P_8 = 8 × 2 sin(π/8) ≈ 6.12
  87    Q_8 = 8 × 2 tan(π/8) ≈ 6.63
  88
  89    3.06 < π < 3.31 (bounds from 8-gon) -/

depends on (1)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use