lean_workbook_plus_14517
ProvedIf where , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14517 : ∀ x a : ℝ, (x = x * a ∧ a < 1) → x = 0 := by sorry
Source
If where , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14517 : ∀ x a : ℝ, (x = x * a ∧ a < 1) → x = 0 := by sorry