theorem
proved
totient_two
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 465.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
462/-! ### Additional totient values -/
463
464/-- φ(2) = 1. -/
465theorem totient_two : totient 2 = 1 := by
466 simp [totient]
467
468/-- φ(3) = 2. -/
469theorem totient_three : totient 3 = 2 := by
470 native_decide
471
472/-- φ(4) = 2. -/
473theorem totient_four : totient 4 = 2 := by
474 native_decide
475
476/-- φ(5) = 4. -/
477theorem totient_five : totient 5 = 4 := by
478 native_decide
479
480/-- φ(6) = 2. -/
481theorem totient_six : totient 6 = 2 := by
482 native_decide
483
484/-- φ(8) = 4. -/
485theorem totient_eight : totient 8 = 4 := by
486 native_decide
487
488/-- φ(45) = 24. -/
489theorem totient_fortyfive : totient 45 = 24 := by
490 native_decide
491
492/-- φ(360) = 96. -/
493theorem totient_threehundredsixty : totient 360 = 96 := by
494 native_decide
495