Theorems · Theorem · commutative algebra

HahnModule.coeff_single_zero_smul

∀ {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ'] [inst_1 : AddCommMonoid V] {Γ : Type u_6}
  [inst_2 : AddCommMonoid Γ] [inst_3 : PartialOrder Γ] [inst_4 : AddAction Γ Γ'] [inst_5 : IsOrderedCancelVAdd Γ Γ']
  [inst_6 : MulZeroClass R] [inst_7 : SMulWithZero R V] {r : R} {x : HahnModule Γ' R V} {a : Γ'},
  ((HahnModule.of R).symm ((HahnSeries.single 0) r • x)).coeff a = r • ((HahnModule.of R).symm x).coeff a

Defined in

Mathlib.RingTheory.HahnSeries.Multiplication

Cited by

2 results in Mathlib

Foundations

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

Assumes

PartialOrderAddCommMonoidAddCommMonoidPartialOrderAddActionIsOrderedCancelVAddMulZeroClassSMulWithZero