Theorems · Theorem · commutative algebra

HahnSeries.SummableFamily.powers_toFun

∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R) (n : ℕ),
  (HahnSeries.SummableFamily.powers x) n = (if 0 < x.orderTop then x else 0) ^ n

Defined in

Mathlib.RingTheory.HahnSeries.Summable

Cited by

14 results in Mathlib

Foundations

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

Assumes

AddCommMonoidLinearOrderIsOrderedCancelAddMonoidCommRing