Prove2Me

lean_workbook_plus_22032

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

(S2 : (P(x),Q(x))=(cx,cx+d)∀x)(P(x),Q(x))=(cx,cx+d)\quad\forall x) whatever are c,d∈Rc,d\in\mathbb R , c≠0c\ne 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_22032 (c d : ℝ) (hc : c ≠ 0) (P Q : ℝ → ℝ) (hPQ: ∀ x, (P x, Q x) = (c * x, c * x + d)) : ∃ c' d', c' ≠ 0 ∧ ∀ x, (P x, Q x) = (c' * x, c' * x + d')   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph