Theorems · Definition · commutative algebra

PowerSeries.weierstrassUnit

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

The h in the Weierstrass preparation theorem.

Defined in: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Cited by: 8 results in Mathlib
Foundations: Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsLocalRing IsAdicComplete

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
CommRingstatement and proof · cited by 17,173
RingHomstatement · cited by 10,189
PowerSeriesstatement and proof · cited by 797
IsLocalRingstatement and proof · cited by 339
IsLocalRing.maximalIdealstatement and proof · cited by 297
IsLocalRing.ResidueFieldstatement · cited by 156
IsAdicCompletestatement and proof · cited by 124
PowerSeries.mapstatement and proof · cited by 82
IsLocalRing.residuestatement and proof · cited by 71

Cited by8

Results whose statement or proof uses this declaration.

PowerSeries.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnitstatement · cited by 5
PowerSeries.weierstrassUnit_smulstatement and proof · cited by 0
PowerSeries.isUnit_weierstrassUnitstatement · cited by 0
PowerSeries.IsWeierstrassFactorization.uniquestatement · cited by 0
PowerSeries.weierstrassDistinguished_mulproof · cited by 0
PowerSeries.eq_weierstrassDistinguished_mul_weierstrassUnitstatement · cited by 0
PowerSeries.weierstrassDistinguished_smulproof · cited by 0
PowerSeries.weierstrassUnit_mulstatement and proof · cited by 0