Theorems · Theorem · commutative algebra

HahnModule.coeff_smul_order_add_order

∀ {R : Type u_3} {V : Type u_5} [inst : AddCommMonoid V] {Γ : Type u_6} [inst_1 : AddCommMonoid Γ]
  [inst_2 : LinearOrder Γ] [inst_3 : IsOrderedCancelAddMonoid Γ] [inst_4 : Zero R] [inst_5 : SMulWithZero R V]
  (x : HahnSeries Γ R) (y : HahnModule Γ R V),
  ((HahnModule.of R).symm (x • y)).coeff (x.order + ((HahnModule.of R).symm y).order) =
    x.leadingCoeff • ((HahnModule.of R).symm y).leadingCoeff

Defined in

Mathlib.RingTheory.HahnSeries.Multiplication

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoidLinearOrderIsOrderedCancelAddMonoidZeroSMulWithZero