Lean-Workbook Plus 61458: Totient preserves divisibility

Proved

WorkbookRestored.plus_61458

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For natural numbers $d,n$ , if $d\mid n$ then $\varphi(d)\mid\varphi(n)$ .

Source: Lean-Workbook row lean_workbook_plus_61458 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble

import Mathlib.Data.Nat.Totient
open Nat

Formal statement

theorem WorkbookRestored.plus_61458 {d n : ℕ} (h : d ∣ n) : totient d ∣ totient n   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_61458; immutable original Prove2Me node 6210b3f3-9f34-4842-b00e-bed319877091

View graph