IntegerLocalDivisibility.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Reflecting prime-power divisibility from the localized integers

A denominator inverted in the localization at (p) is not divisible by p. Clearing that denominator and using primality therefore reflects divisibility by every power of p back to the integers. The argument includes the zeroth power and the zero numerator, without any nonzero numerator hypothesis.

theorem OAI.CirculantHadamard.integer_prime_pow_dvd_of_localization line 22

Source documentation

Divisibility by a rational prime power in its actual integer localization implies the same divisibility in the integers.

theorem integer_prime_pow_dvd_of_localization
    {A : Type uA} [CommRing A] [Algebra ℤ A]
    {P : Ideal ℤ} [P.IsPrime] [IsLocalization.AtPrime A P]
    {p : ℕ} (hp : p.Prime) (hP : P = Ideal.span ({(p : ℤ)} : Set ℤ))
    (t : ℕ) (x : ℤ) (hx : (p : A) ^ t ∣ algebraMap ℤ A x) :
    (p : ℤ) ^ t ∣ x := by
…

theorem OAI.CirculantHadamard.integer_prime_pow_dvd_localization_iff line 45

Source documentation

Prime-power divisibility of integer coefficients is unchanged by localization at that prime.

theorem integer_prime_pow_dvd_localization_iff
    {A : Type uA} [CommRing A] [Algebra ℤ A]
    {P : Ideal ℤ} [P.IsPrime] [IsLocalization.AtPrime A P]
    {p : ℕ} (hp : p.Prime) (hP : P = Ideal.span ({(p : ℤ)} : Set ℤ))
    (t : ℕ) (x : ℤ) :
    (p : A) ^ t ∣ algebraMap ℤ A x ↔ (p : ℤ) ^ t ∣ x := by
…