Is there an easy way to get obvious instances on structures?

Stream: new members

[Scott Carnahan]

I have been using the following structure with no problems:

import Mathlib.Algebra.Module.LinearMap
import Mathlib.RingTheory.HahnSeries

structure VertexOperator (R : Type*) (V : Type*) [CommRing R] [AddCommGroup V] [Module R V] where
  toMap : V →ₗ[R] HahnSeries ℤ V

but building up to instance [CommRing R] [AddCommGroup V] [Module R V] : Module R (VertexOperator R V) took about 100 lines of code with lots of ext, intro and simp to deal with the various fields. It seems that linear maps already have an R-module structure, but my use of structure means this fact is obscured. Is there an easier way to get an R-module action?

[Eric Wieser]

You want to end up using docs#Function.Injective.addCommGroup and docs#Function.Injective.module

[Eric Wieser]

Though the easiest option by far is abbrev VertexOperator := V →ₗ[R] HahnSeries ℤ V

[Scott Carnahan]

Are there downsides to abbrev?

[Eric Wieser]

Whether that's a good idea depends on whether there are behaviors that make sense for VertexOperator R V which do not make sense for V →ₗ[R] HahnSeries ℤ V

[Eric Wieser]

For instance, we can't use it for abbrev Polynomial := Finsupp ... because we want * to mean different things on polynomials (convolutive) and supported functions (pointwise)

[Scott Carnahan]

I see. Thanks!

[Eric Wieser]

Actually, here you could use docs#Equiv.module