Theorems · Definition · commutative algebra

HahnSeries.SummableFamily.hsum

{Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} →
      [inst : PartialOrder Γ] → [inst_1 : AddCommMonoid R] → HahnSeries.SummableFamily Γ R α → HahnSeries Γ R

The infinite sum of a SummableFamily of Hahn series.

Defined in: Mathlib.RingTheory.HahnSeries.Summable
Cited by: 39 results in Mathlib
Foundations: Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PartialOrder AddCommMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
AddCommMonoidstatement and proof · cited by 12,281
PartialOrderstatement and proof · cited by 6,410
HahnSeriesstatement · cited by 528
finsumproof · cited by 286
HahnSeries.coeffproof · cited by 235
HahnSeries.SummableFamilystatement and proof · cited by 88

Cited by41

Results whose statement or proof uses this declaration.

PowerSeries.hevalproof · cited by 7
HahnSeries.SummableFamily.coeff_hsumstatement · cited by 7
HahnSeries.SummableFamily.coeff_hsum_eq_sumstatement · cited by 4
HahnSeries.SummableFamily.orderTop_hsum_binomialFamily_posstatement and proof · cited by 3
HahnSeries.inv_singleproof · cited by 3
PowerSeries.heval_applystatement · cited by 3
HahnSeries.SummableFamily.hsum_mulstatement and proof · cited by 2
HahnSeries.SummableFamily.hsum_orderTop_of_lestatement and proof · cited by 2
HahnSeries.SummableFamily.lsumproof · cited by 2
HahnSeries.SummableFamily.one_sub_self_mul_hsum_powersstatement and proof · cited by 2
HahnSeries.SummableFamily.smul_hsumstatement and proof · cited by 2
HahnSeries.SummableFamily.coeff_smulstatement and proof · cited by 2