isWeierstrassDivisorAt' — Mathlib

English

If g is distinguished at I, then g.toPowerSeries is Weierstrass divisor at I, under suitable Hausdorff condition; otherwise, reduce to previous case.

Русский

Если g IsDistinguishedAt I, то g.toPowerSeries является дивизором Вайершстраса при I при соответствующем условии Хаусдорфа; иначе переход к предыдущему случаю.

LaTeX

$$$\\forall {A} [\\text{CommRing } A], \\; (H : g.IsDistinguishedAt I) [IsHausdorff I A] \\Rightarrow IsWeierstrassDivisorAt g I$$$

Lean4

theorem _root_.Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt' {g : A[X]} {I : Ideal A} (H : g.IsDistinguishedAt I)
    [IsHausdorff I A] : IsWeierstrassDivisorAt g I :=
  by
  rcases eq_or_ne I ⊤ with rfl | hI
  · have := ‹IsHausdorff ⊤ A›.subsingleton
    exact isUnit_of_subsingleton _
  exact H.isWeierstrassDivisorAt hI

Похожие утверждения