Theorems · Theorem · commutative algebra
PowerSeries.X_pow_dvd_iff
∀ {R : Type u_1} [inst : Semiring R] {n : ℕ} {φ : PowerSeries R},
PowerSeries.X ^ n ∣ φ ↔ ∀ m < n, (PowerSeries.coeff m) φ = 0- Defined in
- Mathlib.RingTheory.PowerSeries.Basic
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
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
- RingHom.idstatement and proof · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- LinearMapstatement and proof · cited by 10,215
- Finsuppproof · cited by 5,255
- Finsupp.singleproof · cited by 943
- PowerSeriesstatement and proof · cited by 797
- MvPowerSeriesproof · cited by 659
- DFunLikeproof · cited by 576
- PowerSeries.coeffstatement and proof · cited by 324
- MvPowerSeries.coeffproof · cited by 273
- PowerSeries.Xstatement and proof · cited by 183
Cited by4
Results whose statement or proof uses this declaration.
- PowerSeries.X_dvd_iffproof · cited by 5
- LaurentSeries.intValuation_le_iff_coeff_lt_eq_zeroproof · cited by 3
- PowerSeries.subst_substInv_rightproof · cited by 2
- LaurentSeries.coeff_zero_of_lt_intValuationproof · cited by 0