def CarmichaelTotient.HasUniquePositiveTotientPreimage (n : ℕ) : Prop

n has exactly one positive preimage under Euler's totient function.

Equations

• CarmichaelTotient.HasUniquePositiveTotientPreimage n = ∃! m : ℕ, 0 < m ∧ m.totient = n

def CarmichaelTotient.HasAtLeastTwoPositiveTotientPreimages (n : ℕ) : Prop

n has at least two distinct positive preimages under Euler's totient function.

Equations

• CarmichaelTotient.HasAtLeastTwoPositiveTotientPreimages n = ∃ (a : ℕ) (b : ℕ), a ≠ b ∧ 0 < a ∧ 0 < b ∧ a.totient = n ∧ b.totient = n