Documentation

CarmichaelTotient.Basic

source
theorem CarmichaelTotient.hasAtLeastTwoPositiveTotientPreimages_one :
HasAtLeastTwoPositiveTotientPreimages 1
source
theorem CarmichaelTotient.hasAtLeastTwoPositiveTotientPreimages_two :
HasAtLeastTwoPositiveTotientPreimages 2
source
theorem CarmichaelTotient.not_hasUnique_of_hasAtLeastTwo {n : ℕ} (h : HasAtLeastTwoPositiveTotientPreimages n) :
¬HasUniquePositiveTotientPreimage n
source
theorem CarmichaelTotient.not_hasUniquePositiveTotientPreimage_zero :
¬HasUniquePositiveTotientPreimage 0
source
theorem CarmichaelTotient.not_hasUniquePositiveTotientPreimage_one :
¬HasUniquePositiveTotientPreimage 1
source
theorem CarmichaelTotient.not_hasUniquePositiveTotientPreimage_two :
¬HasUniquePositiveTotientPreimage 2