## Stream: general

### Topic: Module refactor

#### Kenny Lau (Jan 08 2019 at 14:29):

I have refactored modules in order to make it possible for a module to be based on two rings. However, there is a small part in analysis/normed_space written by @Patrick Massot and @Johannes Hölzl which I do not know how to fix. I would be grateful if they could kindly offer their assistance.

#### Kenny Lau (Jan 26 2019 at 03:41):

I am rebasing it to the current mathlib; I would appreciate it if we could pause merging module-related stuff for a while (that would include my recent #625)

#### Kenny Lau (Jan 26 2019 at 03:41):

@Mario Carneiro do you think this is a good time?

#### Mario Carneiro (Jan 26 2019 at 03:42):

sure, what's the status?

#### Kenny Lau (Jan 26 2019 at 03:43):

expect a PR in 10 minutes

make that 1 hour

#626

yes

#### Kenny Lau (Jan 26 2019 at 11:38):

@Mario Carneiro pi_instance fails for smul because pi_instance tries to apply has_scalar.smul but it fails because the instance cannot be synthesized

#### Kenny Lau (Jan 26 2019 at 14:52):

• The first parameters of has_scalar, semimodule, module, and vector_space are no longer out_params. The implication is that the base ring will have to be inferred either from being provided explicitly or from context.
• The base ring of linear maps are now specified via β →ₗ[α] γ, alongside the original notation β →ₗ γ. A similar notation has been introduced for tensor products.
• The base ring in some definitions/theorems are made explicit.

#### Kenny Lau (Jan 26 2019 at 14:52):

do you guys have any suggestions / objections?

@Kevin Buzzard

#### Kevin Buzzard (Jan 26 2019 at 20:09):

In real life one often sees phrases like "$R$-linear maps from $M$ to $N$" so I'm very happy. I live in a world where one often can consider both $R$-linear and $S$-linear maps between two modules.

#### Kenny Lau (Jan 26 2019 at 21:40):

I am rebasing it to the current mathlib; I would appreciate it if we could pause merging module-related stuff for a while (that would include my recent #625)

Kenny Lau, 2019 Jan 26 03:41 (UTC) :point_up:

I hope I didn't start a one-month module hiatus

Last updated: May 18 2021 at 17:44 UTC