Theorems · Theorem · commutative algebra

MvPowerSeries.le_weightedOrder_subst

∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} (w : τ → ℕ),
  MvPowerSeries.HasSubst a →
    ∀ (f : MvPowerSeries σ R),
      ⨅ d, ⨅ (_ : (MvPowerSeries.coeff d) f ≠ 0), (Finsupp.weight (MvPowerSeries.weightedOrder w ∘ a)) d ≤
        MvPowerSeries.weightedOrder w (MvPowerSeries.subst a f)

Defined in: Mathlib.RingTheory.MvPowerSeries.Substitution
Cited by: 3 results in Mathlib
Foundations: Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites31

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
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
LinearMapstatement · cited by 10,215
Finsuppstatement and proof · cited by 5,255
ENatstatement · cited by 4,985
AddMonoidHomstatement · cited by 3,230
LE.le.transproof · cited by 3,151
Finset.sum_congrproof · cited by 2,323
iInfstatement and proof · cited by 1,690
Finsupp.supportproof · cited by 828

Cited by3

Results whose statement or proof uses this declaration.

MvPowerSeries.le_order_substproof · cited by 1
MvPowerSeries.le_weightedOrder_subst_of_forall_ne_zeroproof · cited by 0
PowerSeries.le_weightedOrder_substproof · cited by 0