toPowerSeriesAlg — Mathlib

English

There is an isomorphism of algebras between HahnSeries Nat A and PowerSeries A.

Русский

Существует изоморфизм алгебр между HahnSeries Nat A и PowerSeries A.

LaTeX

$$$HahnSeries\\,Nat\\,A \\cong_{A} PowerSeries A$$$

Lean4

/-- The `R`-algebra `HahnSeries ℕ A` is isomorphic to `PowerSeries A`. -/
@[simps!]
def toPowerSeriesAlg : HahnSeries ℕ A ≃ₐ[R] PowerSeries A :=
  { toPowerSeries with
    commutes' := fun r => by
      ext n
      cases n <;> simp [algebraMap_apply, PowerSeries.algebraMap_apply] }

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