The units digit of a digit-product equation
ProvedWorkbookSource.plus_76401lean-workbooksource-checked
Let denote the product of the digits of a number, and denote the sum of the digits of a number. For example, and . Suppose is a two-digit number such that What is the units digit of
Source: InternLM Lean-Workbook, record lean_workbook_plus_76401 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.plus_76401 (a b n : ℕ) (h₀ : 1 ≤ a ∧ a ≤ 9) (h₁ : 0 ≤ b ∧ b ≤ 9) (h₂ : n = 10 * a + b) (h₃ : n = a * b + a + b) : b = 9 := by sorry
Source