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.
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)
: