Divisibility in commutative rings

Divisibility up to a unit and a multiple of the divisor

In a commutative ring, whether a divides an element does not change when a multiple of a is added to it and the result is multiplied by a unit. This combines IsUnit.dvd_mul_left with dvd_add_left, in the shape produced by transformation formulas such as those of a change of variables of a Weierstrass equation, where the new coefficient is a unit times the old one plus a correction term.

Divisibility of powers by successive integers

If p ∣ s ^ (p - 1) for a prime p and every natural number prime to p is a unit, then n + 1 ∣ sⁿ for every n. This is the condition under which the denominators n + 1 of a logarithm ∑ aₙ Tⁿ⁺¹ / (n + 1) are cancelled after rescaling T by s. For the ring of integers of a finite extension of ℚ_p with normalised valuation v, it asks v(s) ≥ v(p) / (p - 1).

Main results

• IsUnit.dvd_iff_of_eq_mul_add: if y = v * (x + a * z) with v a unit, then a ∣ y ↔ a ∣ x.
• TauCeti.natCast_add_one_dvd_pow: a sufficient condition for n + 1 ∣ sⁿ for every n.

theorem IsUnit.dvd_iff_of_eq_mul_add {R : Type u_1} [CommRing R] {a x y v : R} (hv : IsUnit v) (z : R) (h : y = v * (x + a * z)) : a ∣ y ↔ a ∣ x

Divisibility by a is unchanged by adding a multiple of a and multiplying by a unit: if y = v * (x + a * z) with v a unit, then a ∣ y ↔ a ∣ x.

theorem TauCeti.natCast_add_one_dvd_pow {R : Type u_2} [CommSemiring R] {p : ℕ} (hp : Nat.Prime p) {s : R} (hs : ↑p ∣ s ^ (p - 1)) (hR : ∀ (m : ℕ), p.Coprime m → IsUnit ↑m) (n : ℕ) : ↑n + 1 ∣ s ^ n

n + 1 divides sⁿ for every n, if p ∣ s ^ (p - 1) for a prime p and every natural number prime to p is a unit.