Theorems · Theorem · commutative algebra

MvPowerSeries.coeff_mul_left_one_sub_of_lt_weightedOrder

∀ {σ : Type u_1} (w : σ → ℕ) {R : Type u_3} [inst : Ring R] {f g : MvPowerSeries σ R} {d : σ →₀ ℕ},
  ↑((Finsupp.weight w) d) < MvPowerSeries.weightedOrder w g →
    (MvPowerSeries.coeff d) (f * (1 - g)) = (MvPowerSeries.coeff d) f

Defined in: Mathlib.RingTheory.MvPowerSeries.Order
Cited by: 2 results in Mathlib
Foundations: Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites18

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 · cited by 18,349
LinearMapstatement · cited by 10,215
Ringstatement and proof · cited by 7,463
Finsuppstatement and proof · cited by 5,255
ENatstatement · cited by 4,985
mul_oneproof · cited by 3,885
AddMonoidHomstatement · cited by 3,230
MvPowerSeriesstatement and proof · cited by 659
map_subproof · cited by 565
lt_of_lt_of_leproof · cited by 438
MvPowerSeries.coeffstatement and proof · cited by 273

Cited by2

Results whose statement or proof uses this declaration.

MvPowerSeries.coeff_mul_prod_one_sub_of_lt_weightedOrderproof · cited by 1
MvPowerSeries.coeff_mul_left_one_sub_of_lt_orderproof · cited by 0