theorem proved term proof

`totient_onehundredtwenty`

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

formal statement (Lean)

1027theorem totient_onehundredtwenty : totient 120 = 32 := by native_decide

Term-mode proof.

1028
1029/-! ### Liouville at small composites -/
1030
1031/-- λ(6) = 1 (6 = 2 × 3, Ω(6) = 2, even). -/

Lean names referenced from this declaration's body.

totient in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use