padicNorm.padicNorm_of_prime_of_ne
theorem padicNorm.padicNorm_of_prime_of_ne :
∀ {p q : ℕ} [p_prime : Fact p.Prime] [q_prime : Fact q.Prime], p ≠ q → padicNorm p ↑q = 1
This theorem states that for any two prime numbers `p` and `q`, if `p` is not equal to `q`, then the `p`-adic norm of `q` is `1`. In mathematical terms, if $p$ and $q$ are distinct prime numbers, then the `p`-adic norm of `q`, denoted as $\|q\|_p$, equals `1`.
More concisely: For distinct prime numbers p and q, their p-adic norms are equal to 1: $\|q\|_p = 1$, where p and q are prime numbers and q ≠ p.
|
padicNorm.eq_zpow_of_nonzero
theorem padicNorm.eq_zpow_of_nonzero : ∀ {p : ℕ} {q : ℚ}, q ≠ 0 → padicNorm p q = ↑p ^ (-padicValRat p q)
This theorem describes the `p`-adic norm of a rational number `q` when `q` is not zero. Specifically, for any natural number `p` and any rational number `q`, if `q` is not equal to zero, then the `p`-adic norm of `q` is equal to `p` raised to the power of the negative of the `p`-adic valuation of `q`. The `p`-adic valuation of `q` is the difference between the `p`-adic valuation of the numerator of `q` and the `p`-adic valuation of the denominator of `q`.
More concisely: For any natural number $p$ and rational number $q \neq 0$, the $p$-adic norm of $q$ is equal to $p^{-\text{vp}(q)}$, where $\text{vp}(q) = \text{vp}(q_\text{num}) - \text{vp}(q_\text{den})$, and $\text{vp}(x)$ denotes the $p$-adic valuation of $x$.
|
padicNorm.padicNorm_p
theorem padicNorm.padicNorm_p : ∀ {p : ℕ}, 1 < p → padicNorm p ↑p = (↑p)⁻¹
This theorem states that for any natural number 'p' greater than 1, the p-adic norm of 'p' is equal to the inverse of 'p'. There is also another version of this theorem that applies when 'p' is prime, referred to as `padicNorm.padicNorm_p_of_prime`.
More concisely: For any prime number p, the p-adic norm of p is equal to p^(-1) in the p-adic number system.
|
padicNorm.padicNorm_p_of_prime
theorem padicNorm.padicNorm_p_of_prime : ∀ {p : ℕ} [inst : Fact p.Prime], padicNorm p ↑p = (↑p)⁻¹
The theorem `padicNorm.padicNorm_p_of_prime` states that for any prime number `p`, the `p`-adic norm of `p` is `p⁻¹`. In other words, when `p` is a prime number, the `p`-adic norm applied to `p` returns the reciprocal of `p`. This theorem also suggests a more specific version, `padicNorm.padicNorm_p`, which assumes `1 < p`.
More concisely: For any prime number `p`, the `p`-adic norm of `p` equals `p⁻¹`.
|
padicNorm.div
theorem padicNorm.div : ∀ {p : ℕ} [hp : Fact p.Prime] (q r : ℚ), padicNorm p (q / r) = padicNorm p q / padicNorm p r
This theorem states that the p-adic norm has the property of respecting division. Specifically, for any prime number `p` and any two rational numbers `q` and `r`, the p-adic norm of the quotient of `q` and `r` is equal to the quotient of the p-adic norms of `q` and `r`. This theorem is predominantly about how the p-adic norm behaves under division; it exhibits similar behavior as the typical absolute value operation.
More concisely: For any prime number `p`, the p-adic norm of the quotient of two rational numbers `q` and `r` is equal to the quotient of their p-adic norms: `|q/r|_p = |q|_p / |r|_p`.
|
padicNorm.add_eq_max_of_ne
theorem padicNorm.add_eq_max_of_ne :
∀ {p : ℕ} [hp : Fact p.Prime] {q r : ℚ},
padicNorm p q ≠ padicNorm p r → padicNorm p (q + r) = max (padicNorm p q) (padicNorm p r)
The theorem `padicNorm.add_eq_max_of_ne` states that for any prime number `p` and any two rational numbers `q` and `r`, if the `p`-adic norms of `q` and `r` are not equal, then the `p`-adic norm of the sum of `q` and `r` (i.e., `q + r`) is equal to the maximum of the `p`-adic norms of `q` and `r`. In other words, if $||q||_p$ and $||r||_p$ are not equal, then $||q + r||_p = \max\{||q||_p, ||r||_p\}$. The `p`-adic norm is a measure of size for rational numbers, based on their divisibility by a given prime number `p`.
More concisely: For any prime number `p` and rational numbers `q` and `r` with unequal `p`-adic norms, the `p`-adic norm of their sum equals the maximum of their individual `p`-adic norms.
|
padicNorm.mul
theorem padicNorm.mul : ∀ {p : ℕ} [hp : Fact p.Prime] (q r : ℚ), padicNorm p (q * r) = padicNorm p q * padicNorm p r
The theorem 'padicNorm.mul' states that the `p`-adic norm is multiplicative for any prime number `p` and any two rational numbers `q` and `r`. In other words, the `p`-adic norm of the product of `q` and `r` is equal to the product of the `p`-adic norms of `q` and `r`. This is an important property of `p`-adic norms in number theory, and it highlights their behavior under multiplication.
More concisely: The `p`-adic norm of the product of two rational numbers is equal to the product of their individual `p`-adic norms.
|
padicNorm.one
theorem padicNorm.one : ∀ {p : ℕ}, padicNorm p 1 = 1
This theorem states that for all natural numbers `p`, the `p`-adic norm of `1` is `1`. This means that regardless of the prime number `p` you choose, when you calculate the `p`-adic norm for the rational number `1`, the result will always be `1`.
More concisely: For all natural numbers p, the p-adic norm of 1 is equal to 1.
|
padicNorm.of_int
theorem padicNorm.of_int : ∀ {p : ℕ} [hp : Fact p.Prime] (z : ℤ), padicNorm p ↑z ≤ 1
This theorem states that for any prime number `p` and any integer `z`, the `p`-adic norm of `z` is less than or equal to `1`. The `p`-adic norm is a function that takes a prime number `p` and a rational number `q`, and returns a rational number that is defined as `p` to the power of the negative of the `p`-adic valuation of `q` if `q` is not zero; if `q` is zero, the `p`-adic norm is `0`. Therefore, this theorem asserts a specific property of the `p`-adic norm when the input is an integer.
More concisely: For any prime number `p` and integer `z`, the `p`-adic norm of `z` is less than or equal to 1.
|
padicNorm.nonneg
theorem padicNorm.nonneg : ∀ {p : ℕ} (q : ℚ), 0 ≤ padicNorm p q
The theorem `padicNorm.nonneg` states that the `p`-adic norm is always nonnegative. In other words, for any natural number `p` and any rational number `q`, the `p`-adic norm of `q` (defined as `p` to the power of negative `padicValRat p q` if `q` is not zero, and `0` if `q` is zero) is always greater than or equal to `0`.
More concisely: For any prime number p and rational number q, the p-adic norm of q is non-negative, that is, |q|\_p ≥ 0.
|
padicNorm.padicNorm_p_lt_one
theorem padicNorm.padicNorm_p_lt_one : ∀ {p : ℕ}, 1 < p → padicNorm p ↑p < 1
This theorem states that for any natural number `p` greater than 1, the `p`-adic norm of `p` is less than 1. There is also a related theorem, `padicNorm.padicNorm_p_lt_one_of_prime`, which gives the same result under the assumption that `p` is a prime number.
In mathematical terms, if `p` is a natural number greater than 1, then the `p`-adic norm of `p`, denoted as `||p||_p`, is less than 1.
More concisely: For any prime number `p` greater than 1, the `p`-adic norm of `p` is strictly less than 1.
|
padicNorm.sub
theorem padicNorm.sub :
∀ {p : ℕ} [hp : Fact p.Prime] {q r : ℚ}, padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm p r)
The theorem `padicNorm.sub` states that for any prime natural number `p` and any two rational numbers `q` and `r`, the `p`-adic norm of the difference between `q` and `r` is less than or equal to the maximum of the `p`-adic norms of `q` and `r`. In other words, this theorem is a restatement of the Archimedean property for the `p`-adic norm.
More concisely: The `p`-adic norm of the difference between two rational numbers is less than or equal to the maximum of their individual `p`-adic norms.
|
padicNorm.neg
theorem padicNorm.neg : ∀ {p : ℕ} (q : ℚ), padicNorm p (-q) = padicNorm p q
The theorem `padicNorm.neg` states that the p-adic norm function `padicNorm p` is symmetric with respect to the origin. In other words, for any natural number `p` and any rational number `q`, the p-adic norm of `-q` (the negation of `q`) is equal to the p-adic norm of `q`. This implies that the p-adic norm doesn't change if you take the negative of a rational number `q`.
More concisely: For any prime number p and rational number q, the p-adic norm of the negation of q equals the p-adic norm of q.
|
padicNorm.zero_of_padicNorm_eq_zero
theorem padicNorm.zero_of_padicNorm_eq_zero : ∀ {p : ℕ} [hp : Fact p.Prime] {q : ℚ}, padicNorm p q = 0 → q = 0 := by
sorry
The theorem states that if the `p`-adic norm of a rational number `q` is `0`, then the rational number `q` itself is `0`. Here, `p` is a natural number which is assumed to be prime. The `p`-adic norm is a function that measures a certain 'size' of a rational number, where `p` is a prime number. The size is calculated as `p` raised to the power of the negative `p`-adic valuation of `q` unless `q` is `0`, in which case the `p`-adic norm is defined to be `0`. Thus, if the `p`-adic norm of a rational number `q` equals `0`, it implies that `q` itself is `0`.
More concisely: If the `p`-adic norm of a rational number `q` is 0, then `q` is 0, where `p` is a prime number.
|
padicNorm.nonzero
theorem padicNorm.nonzero : ∀ {p : ℕ} [hp : Fact p.Prime] {q : ℚ}, q ≠ 0 → padicNorm p q ≠ 0
This theorem states that for any non-zero rational number `q` and any prime natural number `p`, the `p`-adic norm of `q` is also non-zero. More formally, given a prime `p` and a rational number `q` such that `q ≠ 0`, the `p`-adic norm, defined as `p` raised to the power of negative `p`-adic valuation of `q`, cannot be zero.
More concisely: For any prime number `p` and non-zero rational number `q`, the `p`-adic norm of `q` is non-zero.
|
padicNorm.values_discrete
theorem padicNorm.values_discrete : ∀ {p : ℕ} {q : ℚ}, q ≠ 0 → ∃ z, padicNorm p q = ↑p ^ (-z)
The theorem `padicNorm.values_discrete` states that for any natural number `p` and any rational number `q` different from zero, there exists an integer `z` such that the `p`-adic norm of `q` (as defined by the `padicNorm` function) equals `p` raised to the power of negative `z`. In other words, the `p`-adic norm of a non-zero rational number takes discrete values of the form `p^-z` for some integer `z`.
More concisely: For any prime number p and non-zero rational number q, there exists an integer z such that the p-adic norm of q equals p^(-z).
|
padicNorm.nonarchimedean
theorem padicNorm.nonarchimedean :
∀ {p : ℕ} [hp : Fact p.Prime] {q r : ℚ}, padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r)
The theorem `padicNorm.nonarchimedean` asserts that the `p`-adic norm is nonarchimedean. This means for any natural number `p` which is a prime number, and for any two rational numbers `q` and `r`, the `p`-adic norm of the sum of `q` and `r` is less than or equal to the maximum of the `p`-adic norm of `q` and the `p`-adic norm of `r`. In mathematical terms, this can be expressed as $\| q + r \|_p \leq \max(\| q \|_p, \| r \|_p)$, where $p$ is a prime number and $q, r \in \mathbb{Q}$.
More concisely: For any prime number p and rational numbers q and r, the p-adic norm of q + r is less than or equal to the maximum of the p-adic norms of q and r. (i.e., \| q + r \|p ≤ max(\| q \|p, \| r \|p)).
|
padicNorm.not_int_of_not_padic_int
theorem padicNorm.not_int_of_not_padic_int :
∀ (p : ℕ) {a : ℚ} [hp : Fact p.Prime], 1 < padicNorm p a → ¬a.isInt = true
This theorem states that for any natural number `p` and any rational number `a`, if `p` is a prime number and the `p`-adic norm of `a` is greater than 1, then `a` is not an integer. In other words, if a rational number is not a `p`-adic integer, then it cannot be an integer. Here, the `p`-adic norm is defined as the power of `p` (where power is negative of the `p`-adic valuation of the rational number), and a rational number is considered a `p`-adic integer if its `p`-adic norm is less than or equal to 1.
More concisely: For any prime number `p` and rational number `a`, if the `p`-adic norm of `a` exceeds 1, then `a` is not an integer.
|
padicNorm.triangle_ineq
theorem padicNorm.triangle_ineq :
∀ {p : ℕ} [hp : Fact p.Prime] (q r : ℚ), padicNorm p (q + r) ≤ padicNorm p q + padicNorm p r
This theorem states that the p-adic norm, a function mapping a natural number 'p' and a rational number 'q' to another rational number, satisfies the triangle inequality. Specifically, for a prime 'p' and any rational numbers 'q' and 'r', the p-adic norm of the sum of 'q' and 'r' is less than or equal to the sum of the p-adic norms of 'q' and 'r' individually. This means that the p-adic norm respects the principle that the "direct distance" between two points is always less than or equal to the "path distance".
More concisely: For any prime number p and rational numbers q and r, the p-adic norm of q + r is less than or equal to the sum of the p-adic norms of q and r.
|
padicNorm.padicNorm_p_lt_one_of_prime
theorem padicNorm.padicNorm_p_lt_one_of_prime : ∀ {p : ℕ} [inst : Fact p.Prime], padicNorm p ↑p < 1
The theorem `padicNorm.padicNorm_p_lt_one_of_prime` states that for any natural number `p` that is prime, the `p`-adic norm of `p` is less than `1`. Here, the `p`-adic norm of a rational number `q` is defined as `p` to the power of the negative of the `p`-adic valuation of `q`, or `0` if `q` equals `0`. The `p`-adic valuation of `q` is the highest power of `p` that divides `q`. This theorem also refers to `padicNorm.padicNorm_p_lt_one`, which has a similar statement but assumes `p` is greater than `1`.
More concisely: For any prime natural number `p`, the `p`-adic norm of `p` is less than 1.
|
padicNorm.nat_eq_one_iff
theorem padicNorm.nat_eq_one_iff : ∀ {p : ℕ} [hp : Fact p.Prime] (m : ℕ), padicNorm p ↑m = 1 ↔ ¬p ∣ m
The theorem `padicNorm.nat_eq_one_iff` states that for any prime number `p` and natural number `m`, the p-adic norm of `m` is equal to one if and only if `p` does not divide `m`. In other words, the p-adic norm of a natural number is 1 if that number is not divisible by the prime number that defines the p-adic norm.
More concisely: For any prime number p and natural number m, the p-adic norm of m is equal to 1 if and only if m is not divisible by p.
|
padicNorm.zero
theorem padicNorm.zero : ∀ {p : ℕ}, padicNorm p 0 = 0
The theorem `padicNorm.zero` states that the p-adic norm of `0` is `0` for any natural number `p`. In other words, for any natural number `p`, when we evaluate the p-adic norm function with `p` and `0` as inputs, the output is `0`.
More concisely: For any prime number p, the p-adic norm of 0 is 0.
|
padicNorm.int_eq_one_iff
theorem padicNorm.int_eq_one_iff : ∀ {p : ℕ} [hp : Fact p.Prime] (m : ℤ), padicNorm p ↑m = 1 ↔ ¬↑p ∣ m
The theorem `padicNorm.int_eq_one_iff` states that for every prime number `p` and every integer `m`, the `p`-adic norm of `m` is equal to one if and only if `p` does not divide `m`. In other words, when we convert the integer `m` into a rational number and compute its `p`-adic norm, we get one if and only if the prime number `p` is not a divisor of `m`.
More concisely: For every prime number p and integer m, the p-adic norm of m equals 1 if and only if p does not divide m.
|