Prove2Me

lean_workbook_plus_37982

Proved

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

If gcd⁡(a,b)=1\gcd(a,b) =1, e∣ace \mid ac and e∣bce \mid bc, then prove that e∣ce \mid c.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_37982 (a b c e : ℕ) (h1 : Nat.Coprime a b) (h2 : e ∣ a*c) (h3 : e ∣ b*c) : e ∣ c   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph