lean_workbook_plus_35402
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35402 (x z : ℝ) : (1 / (3 * x ^ 2) + 3 / z ^ 2) ≥ 2 / (x * z) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_35402 (x z : ℝ) : (1 / (3 * x ^ 2) + 3 / z ^ 2) ≥ 2 / (x * z) := by sorry