Documentation

Iwasawalib.Data.Nat.PrimaryComponent

Primary and prime-to-n component of a natural number (TODO: should go mathlib ???) #

source
def Nat.primaryComponent (n m : ℕ) :
ℕ

The m-primary component for a non-zero natural number n is the largest divisor of n whose prime factors divide m. This number has explicit expression gcd(n, m ^ n).

Equations
Instances For
    source
    def Nat.primeToComponent (n m : ℕ) :
    ℕ

    The prime-to-m component for a non-zero natural number n is the largest divisor of n which is coprime to m.

    Equations
    Instances For
      source
      @[simp]
      theorem Nat.primaryComponent_zero_left (m : ℕ) :
      primaryComponent 0 m = 1
      source
      theorem Nat.primaryComponent_zero_right {n : ℕ} (hn : n ≠ 0) :
      n.primaryComponent 0 = n
      source
      theorem Nat.primaryComponent_pos (n m : ℕ) :
      0 < n.primaryComponent m
      source
      @[simp]
      theorem Nat.primeToComponent_zero_left (m : ℕ) :
      primeToComponent 0 m = 0
      source
      theorem Nat.primeToComponent_zero_right {n : ℕ} (hn : n ≠ 0) :
      n.primeToComponent 0 = 1
      source
      theorem Nat.primaryComponent_dvd_self (n m : ℕ) :
      n.primaryComponent m ∣ n
      source
      theorem Nat.primeToComponent_dvd_self (n m : ℕ) :
      n.primeToComponent m ∣ n
      source
      @[simp]
      theorem Nat.primeToComponent_mul_primaryComponent (n m : ℕ) :
      n.primeToComponent m * n.primaryComponent m = n
      source
      theorem Nat.primaryComponent_eq_div {n : ℕ} (m : ℕ) (hn : n ≠ 0) :
      n.primaryComponent m = n / n.primeToComponent m
      source
      @[simp]
      theorem Nat.primeToComponent_eq_zero_iff (n m : ℕ) :
      n.primeToComponent m = 0 ↔ n = 0
      source
      theorem Nat.primeToComponent_ne_zero_iff (n m : ℕ) :
      n.primeToComponent m ≠ 0 ↔ n ≠ 0
      source
      theorem Nat.primeFactors_primaryComponent_subset {n m : ℕ} (hn : n ≠ 0) (hm : m ≠ 0) :
      (n.primaryComponent m).primeFactors ⊆ m.primeFactors
      source
      theorem Nat.dvd_primaryComponent_iff {n m k : ℕ} (hn : n ≠ 0) (hm : m ≠ 0) :
      k ∣ n.primaryComponent m ↔ k ∣ n ∧ k.primeFactors ⊆ m.primeFactors
      source
      theorem Nat.coprime_primeToComponent_right {n : ℕ} (m : ℕ) (hn : n ≠ 0) :
      (n.primeToComponent m).Coprime m
      source
      theorem Nat.coprime_primeToComponent_primaryComponent (n m : ℕ) :
      (n.primeToComponent m).Coprime (n.primaryComponent m)
      source
      theorem Nat.dvd_primeToComponent_iff {n : ℕ} (m : ℕ) {k : ℕ} (hn : n ≠ 0) :
      k ∣ n.primeToComponent m ↔ k ∣ n ∧ k.Coprime m
      source
      theorem Nat.factorization_primaryComponent (n : ℕ) {m : ℕ} (hm : m ≠ 0) (p : ℕ) :
      (n.primaryComponent m).factorization p = if p ∈ m.primeFactors then n.factorization p else 0
      source
      theorem Nat.factorization_primeToComponent (n : ℕ) {m : ℕ} (hm : m ≠ 0) (p : ℕ) :
      (n.primeToComponent m).factorization p = if p ∈ m.primeFactors then 0 else n.factorization p
      source
      theorem Nat.primaryComponent_eq_prod' (n : ℕ) {m : ℕ} (hm : m ≠ 0) :
      n.primaryComponent m = ∏ p ∈ m.primeFactors, p ^ n.factorization p
      source
      theorem Nat.primaryComponent_eq_prod (n : ℕ) {m : ℕ} (hm : m ≠ 0) :
      n.primaryComponent m = ∏ p ∈ n.primeFactors ∩ m.primeFactors, p ^ n.factorization p
      source
      theorem Nat.primeToComponent_eq_prod {n m : ℕ} (hn : n ≠ 0) (hm : m ≠ 0) :
      n.primeToComponent m = ∏ p ∈ n.primeFactors \ m.primeFactors, p ^ n.factorization p
      source
      theorem Nat.primaryComponent_eq_of_prime (n p : ℕ) [Fact (Prime p)] :
      n.primaryComponent p = p ^ n.factorization p
      source
      theorem Nat.primeToComponent_eq_of_prime (n p : ℕ) [Fact (Prime p)] :
      n.primeToComponent p = n / p ^ n.factorization p