Documentation
CarmichaelTotient
.
SmallCases
Search
return to top
source
Imports
Init
CarmichaelTotient.Basic
Mathlib.Tactic.IntervalCases
Imported by
CarmichaelTotient
.
not_hasUniquePositiveTotientPreimage_le_two
source
theorem
CarmichaelTotient
.
not_hasUniquePositiveTotientPreimage_le_two
{
n
:
ℕ
}
(
hn
:
n
≤
2
)
:
¬
HasUniquePositiveTotientPreimage
n