Notation for Hahn series

Stream: mathlib4

[Violeta Hernández]

Is it possible that we could define some notation for Hahn series? Something like R⟦X^Γ⟧ for HahnSeries Γ R would be my immediate proposal, though I don't know if that might clash with notations for polynomials or other power series.

[Weiyi Wang]

We have an existing "clash" between R[G] (MonoidAlgebra) and R[X] (Polynomial). By analogy it should be fine to have R⟦Γ⟧ For HahnSeries and R⟦X⟧ for PowerSeries

[Violeta Hernández]

Something like this? Mostly just copy-pasting code from MonoidAlgebra here:

@[inherit_doc HahnSeries]
scoped syntax:max (priority := high) term noWs "⟦" term "⟧" : term

macro_rules | `($R⟦$M⟧) => `(HahnSeries $R $M)

/-- Unexpander for `HahnSeries`. -/
@[scoped app_unexpander HahnSeries]
meta def unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $R $M) => `($R[$M])
  | _ => throw ()

[Violeta Hernández]

Wait, this is unfortunate. docs#HahnSeries and docs#MonoidAlgebra use an opposite argument order! R[G] is MonoidAlgebra R G but R⟦Γ⟧ is HahnSeries Γ R.

[Weiyi Wang]

Is that a problem?

[Violeta Hernández]

It's not. Just a mild inconsistency.

[Scott Carnahan]

It seems like a good idea to me.

[Eric Wieser]

Your unexpander has a copy-paste-o