Theorems · Theorem · commutative algebra

HahnSeries.embDomainRingHom_C

∀ {Γ : 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 : NonAssocSemiring R] {f : Γ →+ Γ'} {hfi : Function.Injective ⇑f} {hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g'}
  {r : R}, (HahnSeries.embDomainRingHom f hfi hf) (HahnSeries.C r) = HahnSeries.C r

Defined in

Mathlib.RingTheory.HahnSeries.Multiplication

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidPartialOrderIsOrderedCancelAddMonoidAddCommMonoidPartialOrderIsOrderedCancelAddMonoidNonAssocSemiring