Documentation

Mathlib.RingTheory.PowerSeries.NoZeroDivisors

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⟧.

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

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

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

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

theorem PowerSeries.rescale_injective {R : Type u_1} [CommRing R] [IsDomain R] {a : R} (ha : a 0) :