lean_workbook_plus_24287

Proved

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

Prove that if $a$ and $b$ are coprime, and $a$ is a divisor of $bc$ , then $a$ must be divisible by $c$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24287 (a b c : ℕ) (hab : Nat.Coprime a b) (hbc : b * c ≠ 0) (h : a ∣ b * c) : a ∣ c   :=  by sorry

Source