Theorems · Theorem · commutative algebra

PowerSeries.IsWeierstrassDivisor.of_map_ne_zero

∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} [inst_1 : IsLocalRing A],
  (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 → g.IsWeierstrassDivisor

If g is a power series over a local ring such that its image in the residue field is not zero, then g can be used as a Weierstrass divisor.

Defined in

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Cited by

11 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsLocalRing