Theorems · Definition · commutative algebra
PowerSeries.IsWeierstrassDivisorAt.div
{A : Type u_1} →
[inst : CommRing A] →
{g : PowerSeries A} →
{I : Ideal A} → g.IsWeierstrassDivisorAt I → PowerSeries A → [IsPrecomplete I A] → PowerSeries AThe limit q of the
inductively constructed sequence qₖ in the proof of Weierstrass division.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingIsPrecomplete
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Idealstatement and proof · cited by 4,748
- PowerSeriesstatement and proof · cited by 797
- PowerSeries.mkproof · cited by 52
- IsPrecompletestatement and proof · cited by 29
- PowerSeries.IsWeierstrassDivisorAtstatement and proof · cited by 28
- PowerSeries.IsWeierstrassDivisorAt.divCoeffproof · cited by 3
Cited by20
Results whose statement or proof uses this declaration.
- PowerSeries.IsWeierstrassDivisorAt.modproof · cited by 16
- PowerSeries.weierstrassDivproof · cited by 10
- PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_modstatement and proof · cited by 10
- PowerSeries.IsWeierstrassDivisorAt.div_smulstatement and proof · cited by 2
- PowerSeries.IsWeierstrassDivisorAt.mod_smulproof · cited by 2
- PowerSeries.isWeierstrassDivision_weierstrassDiv_weierstrassModproof · cited by 1
- PowerSeries.exists_isWeierstrassDivisionproof · cited by 1
- PowerSeries.IsWeierstrassDivisorAt.coeff_divstatement · cited by 1
- PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_memstatement and proof · cited by 1
- PowerSeries.IsWeierstrassDivisorAt.div_addstatement and proof · cited by 1
- PowerSeries.IsWeierstrassDivisorAt.div_zerostatement and proof · cited by 1
- PowerSeries.IsWeierstrassDivisorAt.mod_addproof · cited by 1