def definition def or abbrev

`arithmeticMean`

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

formal statement (Lean)

 157noncomputable def arithmeticMean (n₁ n₂ : ℝ) : ℝ := (n₁ + n₂) / 2

Definition body.

 158
 159/-- **F1.4.3**: For distinct positive reals, the geometric mean differs
 160    from the arithmetic mean (AM-GM strict inequality). -/

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

simultaneous_differs_from_sequential in IndisputableMonolith.Foundation.JCostGeometry decl_use

Lean names referenced from this declaration's body.