theorem proved term proof

`totient_one`

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

formal statement (Lean)

 104theorem totient_one : totient 1 = 1 := by

Term-mode proof.

 105  simp [totient, Nat.totient_one]
 106
 107/-- φ(p) = p - 1 for prime p. -/

Lean names referenced from this declaration's body.

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