pith. machine review for the scientific record. sign in
theorem proved term proof

divisors_card_twelve_gt

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

1389theorem divisors_card_twelve_gt : ∀ n, 0 < n → n < 12 → (n : ℕ).divisors.card < (12 : ℕ).divisors.card := by

proof body

Term-mode proof.

1390  intro n hn hlt
1391  interval_cases n <;> native_decide
1392
1393/-! ### More highly composite numbers -/
1394
1395/-- 60 is highly composite (has more divisors than any smaller positive integer). -/

depends on (5)

Lean names referenced from this declaration's body.