82theorem separatelyAdditive_of_interactionDefect_zero 83 {P : ℝ → ℝ → ℝ} (h : ∀ u v : ℝ, interactionDefect P u v = 0) : 84 SeparatelyAdditive P := by
proof body
Term-mode proof.
85 refine ⟨fun u => P u 0 - P 0 0, fun v => P 0 v, ?_⟩ 86 intro u v 87 have h_uv := h u v 88 unfold interactionDefect at h_uv 89 linarith 90 91/-- **Equivalence: separate additivity is identical vanishing of the 92interaction defect.** -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.