theorem proved term proof

`totient_threehundredsixty`

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

formal statement (Lean)

 493theorem totient_threehundredsixty : totient 360 = 96 := by

Term-mode proof.

 494  native_decide
 495
 496/-! ### Ω and ω at prime powers -/
 497
 498/-- Ω(p^k) = k for prime p. -/

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
totient in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use