Theorems · Theorem · commutative algebra

HahnSeries.embDomain_mul

∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  {Γ' : Type u_6} [inst_3 : AddCommMonoid Γ'] [inst_4 : PartialOrder Γ'] [inst_5 : IsOrderedCancelAddMonoid Γ']
  [inst_6 : NonUnitalNonAssocSemiring R] (f : Γ ↪o Γ'),
  (∀ (x y : Γ), f (x + y) = f x + f y) →
    ∀ (x y : HahnSeries Γ R), HahnSeries.embDomain f (x * y) = HahnSeries.embDomain f x * HahnSeries.embDomain f y

Defined in

Mathlib.RingTheory.HahnSeries.Multiplication

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidPartialOrderIsOrderedCancelAddMonoidAddCommMonoidPartialOrderIsOrderedCancelAddMonoidNonUnitalNonAssocSemiring