lean_workbook_plus_37106

Proved

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

in the expression $x = 2^a \cdot 3^b \cdot 5^c \cdot 7^d$ we have $x=1$ only when $a=b=c=d=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37106 (x a b c d : ℕ) (hx : x = 2 ^ a * 3 ^ b * 5 ^ c * 7 ^ d) : x = 1 ↔ a = 0 ∧ b = 0 ∧ c = 0 ∧ d = 0   :=  by sorry

Source