def definition def or abbrev

`boundaryArea`

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

formal statement (Lean)

  84noncomputable def boundaryArea (L : ℝ) : ℝ := 4 * Real.pi * L ^ 2

Definition body.

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

boundaryArea_monotone in IndisputableMonolith.Unification.ConsciousnessBandwidth decl_use
boundaryArea_pos in IndisputableMonolith.Unification.ConsciousnessBandwidth decl_use
maintenanceBudget in IndisputableMonolith.Unification.ConsciousnessBandwidth decl_use

Lean names referenced from this declaration's body.