Theorems · Definition · commutative algebra
PowerSeries.weierstrassDiv
{A : Type u_1} →
[inst : CommRing A] →
[inst_1 : IsLocalRing A] →
PowerSeries A → PowerSeries A → [IsPrecomplete (IsLocalRing.maximalIdeal A) A] → PowerSeries AThe quotient q in Weierstrass division, denoted by f /ʷ g. Note that when the image of
g in the residue field is zero, this is defined to be zero.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound
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.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- PowerSeriesstatement and proof · cited by 797
- IsLocalRingstatement and proof · cited by 339
- IsLocalRing.maximalIdealstatement and proof · cited by 297
- PowerSeries.mapproof · cited by 82
- IsLocalRing.residueproof · cited by 71
- IsPrecompletestatement and proof · cited by 29
- PowerSeries.IsWeierstrassDivisorAt.divproof · cited by 18
- PowerSeries.IsWeierstrassDivisor.of_map_ne_zeroproof · cited by 11
Cited by10
Results whose statement or proof uses this declaration.
- PowerSeries.isWeierstrassDivision_weierstrassDiv_weierstrassModstatement · cited by 1
- PowerSeries.weierstrassDiv_zero_leftstatement · cited by 1
- PowerSeries.weierstrassDiv_zero_rightstatement · cited by 1
- PowerSeries.smul_weierstrassDivstatement · cited by 0
- PowerSeries.zero_weierstrassDivstatement · cited by 0
- PowerSeries.IsWeierstrassDivision.uniquestatement · cited by 0
- PowerSeries.add_weierstrassDivstatement · cited by 0
- PowerSeries.eq_mul_weierstrassDiv_add_weierstrassModstatement · cited by 0
- PowerSeries.weierstrassDiv.congr_simpstatement and proof · cited by 0
- PowerSeries.weierstrassDiv_zerostatement · cited by 0