lean_workbook_plus_31643
Proved.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_31643 (a b c : ℝ) : 3 * a ^ 2 * b ^ 2 + a ^ 2 * c ^ 2 - 8 * b * c ^ 2 * a + b ^ 2 * c ^ 2 + 3 * c ^ 4 ≥ 0 := by sorry
Source
.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_31643 (a b c : ℝ) : 3 * a ^ 2 * b ^ 2 + a ^ 2 * c ^ 2 - 8 * b * c ^ 2 * a + b ^ 2 * c ^ 2 + 3 * c ^ 4 ≥ 0 := by sorry