Nat.totient_pos
theorem Nat.totient_pos : ∀ {n : ℕ}, 0 < n → 0 < n.totient
This theorem states that for any natural number `n`, if `n` is greater than zero, then the value of Euler's totient function at `n` is also greater than zero. Euler's totient function, denoted as `Nat.totient n` in Lean, counts the number of natural numbers strictly less than `n` that are coprime with `n`, i.e., their greatest common divisor is 1. Hence, this theorem asserts that any positive natural number has at least one positive natural number less than itself that is coprime to it.
More concisely: For any natural number `n` greater than zero, the value of Euler's totient function `Nat.totient n` is positive.
|
Nat.totient_prime_pow_succ
theorem Nat.totient_prime_pow_succ : ∀ {p : ℕ}, p.Prime → ∀ (n : ℕ), (p ^ (n + 1)).totient = p ^ n * (p - 1)
This theorem states that for any natural number `p` that is prime, and for any natural number `n`, the totient function applied to `p` raised to the power of `(n + 1)` equals `p` raised to the power of `n` times `(p - 1)`. In mathematical terms, if `p` is a prime number, then φ(`p^(n+1)`) = `p^n * (p - 1)`, where φ is the totient function. The totient function counts the positive integers up to a given integer `n` that are relatively prime to `n`.
More concisely: For any prime number `p` and natural number `n`, the totient function of `p` raised to the power of `(n + 1)` equals `p` raised to the power of `n` multiplied by `p - 1`: φ(`p^(n+1)`) = `p^n * (p - 1)`.
|
Nat.totient_prime
theorem Nat.totient_prime : ∀ {p : ℕ}, p.Prime → p.totient = p - 1
This theorem, `Nat.totient_prime`, states that for every natural number `p`, if `p` is prime, then the value of Euler's totient function at `p` is `p - 1`. Euler's totient function, denoted here as `Nat.totient`, counts the number of natural numbers strictly less than `p` which are coprime with `p`. In other words, the theorem shows that for any prime number `p`, there are `p - 1` numbers less than `p` that share no common factors with `p` apart from 1.
More concisely: For every prime natural number `p`, the number of natural numbers less than `p` coprime to `p` equals `p - 1`.
|
Nat.totient_prime_pow
theorem Nat.totient_prime_pow : ∀ {p : ℕ}, p.Prime → ∀ {n : ℕ}, 0 < n → (p ^ n).totient = p ^ (n - 1) * (p - 1) := by
sorry
The theorem `Nat.totient_prime_pow` states that for a prime number `p` and any natural number `n` greater than 0, Euler's totient function of `p` to the power of `n` is equal to `p` to the power of `(n - 1)` multiplied by `(p - 1)`. In mathematical notation, this is equivalent to the formula $\phi(p^n) = p^{n-1}(p - 1)$, where $\phi$ is Euler's totient function, which counts the number of natural numbers less than `n` that are coprime with `n`.
More concisely: Euler's totient function of a prime number `p` raised to the power `n` equals `p` raised to the power `(n - 1)` multiplied by `(p - 1)`. In other words, $\phi(p^n) = p^{n-1}(p - 1)$, where $\phi$ is Euler's totient function.
|
Nat.totient_eq_card_lt_and_coprime
theorem Nat.totient_eq_card_lt_and_coprime : ∀ (n : ℕ), n.totient = Nat.card ↑{m | m < n ∧ n.Coprime m}
The theorem `Nat.totient_eq_card_lt_and_coprime` characterizes the Euler's totient function, or `Nat.totient`, in terms of set cardinality and coprimality, avoiding the use of `Finset`. Specifically, for any natural number `n`, the value of Euler's totient function `n.totient` is equal to the cardinality of the set of natural numbers `m` that are less than `n` and are coprime to `n`. Here, "coprime" means that `n` and `m` share no common factors other than 1.
More concisely: For any natural number n, the Euler totient function n.totient equals the cardinality of the set of natural numbers m less than n that are coprime to n.
|
Nat.totient_div_of_dvd
theorem Nat.totient_div_of_dvd :
∀ {n d : ℕ}, d ∣ n → (n / d).totient = (Finset.filter (fun k => n.gcd k = d) (Finset.range n)).card
The theorem `Nat.totient_div_of_dvd` states that for any two natural numbers `n` and `d`, if `d` divides `n`, then the Euler's totient function of `n/d` is equal to the cardinality of the set of natural numbers less than `n` that have the greatest common divisor with `n` equal to `d`. In other words, the number of integers less than `n` and co-prime to `n/d` is the same as the number of integers less than `n` whose greatest common divisor with `n` is `d`.
More concisely: For any natural numbers `n` and `d` with `d` dividing `n`, the Euler's totient function `ϕ(n/d)` equals the number of integers less than `n` that are coprime to `n` and have `d` as their greatest common divisor with `n`.
|
Nat.totient_mul_prod_primeFactors
theorem Nat.totient_mul_prod_primeFactors :
∀ (n : ℕ), (n.totient * n.primeFactors.prod fun p => p) = n * n.primeFactors.prod fun p => p - 1
This is Euler's product formula for the totient function. For every natural number `n`, the product of the totient of `n` and the product of `n`'s prime factors is equal to `n` times the product of `n`'s prime factors minus 1. This theorem relates the totient function (which counts the number of integers less than `n` that are coprime to `n`) to the prime factors of `n`, providing a product formula for counting these coprime integers.
More concisely: The totient function of a natural number `n` equals `n` times the product of its prime factors' totients minus the product of its prime factors.
|
ZMod.card_units_eq_totient
theorem ZMod.card_units_eq_totient :
∀ (n : ℕ) [inst : NeZero n] [inst : Fintype (ZMod n)ˣ], Fintype.card (ZMod n)ˣ = n.totient
This theorem states that for a given natural number `n` which is not zero and a finite group of units of integers modulo `n`, denoted as `(ZMod n)ˣ`, the cardinality (number of elements) of this group of units is equal to the Euler's totient function of `n`. In mathematical terms, it states that the order of the multiplicative group of integers modulo `n` is equal to φ(n), where φ is the Euler's totient function, which effectively counts the number of integers less than `n` that are relatively prime to `n`.
More concisely: The order of the multiplicative group of units in ZMod n equals the value of the Euler's totient function φ(n) for a non-zero natural number n.
|
Nat.totient_eq_div_primeFactors_mul
theorem Nat.totient_eq_div_primeFactors_mul :
∀ (n : ℕ), n.totient = (n / n.primeFactors.prod fun p => p) * n.primeFactors.prod fun p => p - 1
This theorem is stating Euler's product formula for the totient function. In terms of number theory, for any natural number 'n', the value of Euler's totient function for 'n' (denoted as `n.totient`) equals the product of `(n / the product of its prime factors)` and `the product of (each prime factor minus 1)`. The totient function counts the positive integers up to a given integer 'n' that are relatively prime to 'n'.
More concisely: The Euler totient function of a natural number n is equal to n multiplied by the reciprocal of the product of all its prime factors raised to the power of their multiplicities.
|
Nat.totient_eq_mul_prod_factors
theorem Nat.totient_eq_mul_prod_factors : ∀ (n : ℕ), ↑n.totient = ↑n * n.primeFactors.prod fun p => 1 - (↑p)⁻¹ := by
sorry
This theorem states Euler's product formula for the totient function. Specifically, for any natural number 'n', it states that the value of the totient function at 'n' is equal to 'n' times the product, over the prime factors of 'n', of the quantity (1 - 1/p), where 'p' is a prime factor of 'n' and the division is a real division.
More concisely: The totient function of a natural number n is equal to n times the product of (1 - 1/p) for all prime factors p of n.
|
Nat.totient_one
theorem Nat.totient_one : Nat.totient 1 = 1
This theorem states that the value of Euler's totient function for the number 1 is equal to 1. Euler's totient function, denoted as $\phi(n)$, counts the number of natural numbers that are less than $n$ and coprime with $n$. In this case, since $1$ is the only natural number less than or equal to $1$ and coprime with $1$, the value of $\phi(1)$ is $1$.
More concisely: The Euler phi function equals 1 for the input 1. (i.e., φ(1) = 1)
|
Nat.totient_eq_prod_factorization
theorem Nat.totient_eq_prod_factorization :
∀ {n : ℕ}, n ≠ 0 → n.totient = n.factorization.prod fun p k => p ^ (k - 1) * (p - 1)
This theorem states Euler's product formula for the totient function. For every nonzero natural number `n`, Euler's totient function `n.totient` equals the product over the factorization of `n`. Specifically, for each prime factor `p` of `n` with multiplicity `k`, the product term is `p` raised to the power of `(k - 1)` times `(p - 1)`. In terms of mathematics, this states that for $n \neq 0$, $\varphi(n) = \prod_{p|n} p^{k-1} \cdot (p - 1)$, where $p$ are the prime factors of $n$ and $k$ is the multiplicity of each prime factor.
More concisely: For every nonzero natural number $n$, the Euler totient function $\varphi(n)$ equals the product of each prime factor $p$ raised to the power of $k-1$ and minus one, where $p$ are the prime factors of $n$ and $k$ is their multiplicity. In other words, $\varphi(n) = \prod\_{p|n} p^{k-1} \cdot (p-1)$.
|