iterateEquiv — Mathlib

English

There is a natural equivalence between the iterated Hahn series and the Hahn series on the lexicographic product.

Русский

Существует естественное эквивалентность между повторно итерационными рядами Ханна и рядом Ханна над лексикографическим произведением.

LaTeX

$$$\mathrm{iterateEquiv} : \mathrm{HahnSeries}_{Γ}(\mathrm{HahnSeries}_{Γ'}(R)) \simeq \mathrm{HahnSeries}_{Lex(Γ\times Γ')} (R)$$$

Lean4

/-- The equivalence between iterated Hahn series and Hahn series on the lex product. -/
@[simps]
def iterateEquiv [PartialOrder Γ'] : HahnSeries Γ (HahnSeries Γ' R) ≃ HahnSeries (Γ ×ₗ Γ') R
    where
  toFun := ofIterate
  invFun := toIterate
  left_inv := congrFun rfl
  right_inv := congrFun rfl

Похожие утверждения