lean_workbook_plus_51761

Open

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

To answer Pocket Sand's question, we use prime factorization for $576$ . Since $576=2^6\cdot 3^2$ , we have $(1+6)(1+2)=21$ positive divisors.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51761 :
  (∑ k in (Nat.divisors 576), 1) = 21   :=  by sorry

Source