Theorems · Definition · commutative algebra

HahnSeries.SummableFamily.smul

{Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      {V : Type u_4} →
        {α : Type u_5} →
          {β : Type u_6} →
            [inst : PartialOrder Γ] →
              [inst_1 : PartialOrder Γ'] →
                [inst_2 : AddCommMonoid V] →
                  [inst_3 : AddCommMonoid R] →
                    [SMulWithZero R V] →
                      [inst_5 : VAdd Γ Γ'] →
                        [IsOrderedCancelVAdd Γ Γ'] →
                          HahnSeries.SummableFamily Γ R α →
                            HahnSeries.SummableFamily Γ' V β → HahnSeries.SummableFamily Γ' V (α × β)

An elementwise scalar multiplication of one summable family on another.

Defined in

Mathlib.RingTheory.HahnSeries.Summable

Cited by

7 results in Mathlib

Foundations

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

Assumes

PartialOrderPartialOrderAddCommMonoidAddCommMonoidSMulWithZeroVAddIsOrderedCancelVAdd