Theorems · Theorem · commutative algebra

HahnModule.of_symm_add

∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : SMul R V] [inst_2 : AddCommMonoid V]
  (x y : HahnModule Γ R V), (HahnModule.of R).symm (x + y) = (HahnModule.of R).symm x + (HahnModule.of R).symm y

Defined in

Mathlib.RingTheory.HahnSeries.Multiplication

Cited by

2 results in Mathlib

Foundations

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

Assumes

PartialOrderSMulAddCommMonoid