Power series over rings with no zero divisors

This file proves, using the properties of orders of power series, that R⟦X⟧ is an integral domain when R is.

We then state various results about R⟦X⟧ with R an integral domain.

Instance

If R has NoZeroDivisors, then so does R⟦X⟧.

instance PowerSeries.instNoZeroDivisors {R : Type u_1} [Semiring R] [NoZeroDivisors R] : NoZeroDivisors (PowerSeries R)

instance PowerSeries.instIsDomain {R : Type u_1} [Ring R] [IsDomain R] : IsDomain (PowerSeries R)

theorem PowerSeries.prime_X {R : Type u_1} [CommRing R] [IsDomain R] : Prime X

The variable of the power series ring over an integral domain is prime.

@[deprecated PowerSeries.prime_X (since := "2026-10-09")]

theorem PowerSeries.X_prime {R : Type u_1} [CommRing R] [IsDomain R] : Prime X

Alias of PowerSeries.prime_X.

---

The variable of the power series ring over an integral domain is prime.

theorem PowerSeries.irreducible_X {R : Type u_1} [CommRing R] [IsDomain R] : Irreducible X

The variable of the power series ring over an integral domain is irreducible.

@[deprecated PowerSeries.irreducible_X (since := "2026-10-09")]

theorem PowerSeries.X_irreducible {R : Type u_1} [CommRing R] [IsDomain R] : Irreducible X

Alias of PowerSeries.irreducible_X.

---

The variable of the power series ring over an integral domain is irreducible.

@[deprecated PowerSeries.prime_X (since := "2026-10-09")]

theorem PowerSeries.span_X_isPrime {R : Type u_1} [CommRing R] [IsDomain R] : (Ideal.span {X}).IsPrime

The ideal spanned by the variable in the power series ring over an integral domain is a prime ideal.

theorem PowerSeries.rescale_injective {R : Type u_1} [CommRing R] [IsDomain R] {a : R} (ha : a ≠ 0) : Function.Injective ⇑(rescale a)