lean_workbook_plus_14790
ProvedLet such that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14790 (f : ℝ → ℝ) (A : Set ℝ) (hA: A = {x : ℝ | ∀ y : ℝ, f (x * y) = x * f y}) : 1 ∈ A := by sorrySource
Let such that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14790 (f : ℝ → ℝ) (A : Set ℝ) (hA: A = {x : ℝ | ∀ y : ℝ, f (x * y) = x * f y}) : 1 ∈ A := by sorry