Theorems · Theorem · commutative algebra

HahnSeries.SummableFamily.support_powerSeriesFamily_subset

∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : CommRing V] [inst_5 : Algebra R V]
  {x : HahnSeries Γ V} (a b : PowerSeries R) (g : Γ),
  ((HahnSeries.SummableFamily.powerSeriesFamily x (a * b)).coeff g).support ⊆
    Finset.image (fun i => i.1 + i.2)
      (((HahnSeries.SummableFamily.powerSeriesFamily x a).mul (HahnSeries.SummableFamily.powerSeriesFamily x b)).coeff
          g).support

Defined in

Mathlib.RingTheory.HahnSeries.HEval

Cited by

1 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidLinearOrderIsOrderedCancelAddMonoidCommRingCommRingAlgebra