lean_workbook_plus_46438
ProvedFind function satisfy:\nf(x)f(y)f(z) = \frac{f(x)}{(x-y)(x-z)} + \frac{f(y)}{(y-x)(y-z)} + \frac{f(z)}{(z-x)(z-y)}\nWith
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_46438 (x y z : ℝ) (h : x ≠ y ∧ y ≠ z ∧ z ≠ x) : ∃ f : ℝ → ℝ, f x * f y * f z = f x / (x - y) / (x - z) + f y / (y - x) / (y - z) + f z / (z - x) / (z - y) := by sorry
Source