PadicInt.maximalIdeal_eq_span_p
theorem PadicInt.maximalIdeal_eq_span_p :
∀ {p : ℕ} [hp : Fact p.Prime], LocalRing.maximalIdeal ℤ_[p] = Ideal.span {↑p}
This theorem states that for any natural number `p` which is proven to be prime (`Nat.Prime p`), the maximal ideal of the local ring of `p`-adic integers (`LocalRing.maximalIdeal ℤ_[p]`) is equivalent to the ideal generated by the set containing `p` (`Ideal.span {↑p}`). In other words, the maximal non-unit elements in the ring of `p`-adic integers are those that can be generated by multiplication with `p`.
More concisely: For any prime natural number `p`, the maximal ideal of the local ring of `p`-adic integers equals the ideal generated by `p`.
|
PadicInt.isUnit_iff
theorem PadicInt.isUnit_iff : ∀ {p : ℕ} [hp : Fact p.Prime] {z : ℤ_[p]}, IsUnit z ↔ ‖z‖ = 1
The theorem `PadicInt.isUnit_iff` states that for any natural number `p` which is a prime number, and any `z` which is a p-adic integer, `z` is a unit (i.e., it has a two-sided inverse) if and only if the norm of `z` (`‖z‖`) is equal to `1`.
More concisely: A p-adic integer `z` is a unit if and only if its norm equals 1 in a p-adic number system, where p is a prime number.
|
PadicInt.norm_le_one
theorem PadicInt.norm_le_one : ∀ {p : ℕ} [inst : Fact p.Prime] (z : ℤ_[p]), ‖z‖ ≤ 1
This theorem states that for any natural number `p` that is prime (indicated by `Fact (Nat.Prime p)`), and any p-adic integer `z` (denoted `ℤ_[p]`), the norm of `z` (denoted `‖z‖`) is less than or equal to 1. In mathematical terms, it asserts that the p-adic norm of any p-adic integer is always less than or equal to 1.
More concisely: For any prime natural number p and any p-adic integer z, the p-adic norm of z is bounded by 1.
|
PadicInt.norm_eq_pow_val
theorem PadicInt.norm_eq_pow_val : ∀ {p : ℕ} [hp : Fact p.Prime] {x : ℤ_[p]}, x ≠ 0 → ‖x‖ = ↑p ^ (-x.valuation) := by
sorry
The theorem `PadicInt.norm_eq_pow_val` states that for any natural number `p` which is prime, and any non-zero `p`-adic integer `x`, the norm of `x` is equal to `p` raised to the power of negative of the `p`-adic valuation of `x`. In other words, for a given prime `p` and a non-zero p-adic integer `x`, the norm of `x` can be calculated by taking `p` to the power of the negation of the `p`-adic valuation of `x`. This establishes a relationship between the norm and the `p`-adic valuation of `p`-adic integers.
More concisely: For any prime number `p` and non-zero `p`-adic integer `x`, the norm of `x` equals `p^(-v_p(x))`, where `v_p(x)` is the `p`-adic valuation of `x`.
|
PadicInt.norm_le_pow_iff_mem_span_pow
theorem PadicInt.norm_le_pow_iff_mem_span_pow :
∀ {p : ℕ} [hp : Fact p.Prime] (x : ℤ_[p]) (n : ℕ), ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
The theorem `PadicInt.norm_le_pow_iff_mem_span_pow` states that for any natural number `p` which is prime, any p-adic integer `x`, and any natural number `n`, the norm of `x` is less than or equal to `p` raised to the power of `-n` if and only if `x` is in the ideal generated by `p^n`. This provides a connection between the p-adic norm of an integer and its membership in certain types of ideals in the ring of p-adic integers.
More concisely: For a prime number p and p-adic integer x, x belongs to the ideal generated by p^n if and only if the norm of x is less than or equal to p^(-n).
|
PadicInt.valuation_nonneg
theorem PadicInt.valuation_nonneg : ∀ {p : ℕ} [hp : Fact p.Prime] (x : ℤ_[p]), 0 ≤ x.valuation
The theorem `PadicInt.valuation_nonneg` states that for any natural number `p` which is prime and for any `p`-adic integer `x`, the `p`-adic valuation of `x` is always non-negative. In other words, when you apply the `p`-adic valuation function to any `p`-adic integer, the result will always be a non-negative integer.
More concisely: For any prime number p and p-adic integer x, the p-adic valuation of x is a non-negative integer.
|
PadicInt.norm_mul
theorem PadicInt.norm_mul : ∀ {p : ℕ} [inst : Fact p.Prime] (z1 z2 : ℤ_[p]), ‖z1 * z2‖ = ‖z1‖ * ‖z2‖
The theorem `PadicInt.norm_mul` states that for any natural number `p` that is a prime number, and any two p-adic integers `z1` and `z2`, the norm or magnitude of the product of `z1` and `z2` is equal to the product of the individual norms of `z1` and `z2`. This is a statement about the properties of p-adic numbers, and specifically, this theorem is asserting that the norm function on the p-adic integers is multiplicative.
More concisely: For any prime number p and p-adic integers z1 and z2, the norm of their product z1 * z2 equals the product of their individual norms.
|