lean_workbook_plus_74009

Proved

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

Let $m \in Z^+$ which satisfy: $a^4 \vdots m \Rightarrow a \vdots m, \forall a \in Z^+$ . Prove that: $a^5 \vdots m \Rightarrow a \vdots m, \forall a \in Z^+$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74009 {m : ℕ} (hm : 0 < m) (h5 : ∀ a : ℕ, 0 < a → a^4 ∣ m → a ∣ m) : ∀ a : ℕ, 0 < a → a^5 ∣ m → a ∣ m   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph