NNRat module structures

Stream: mathlib4

[Scott Carnahan]

It looks like in the 11 weeks between #9951 and #11203 we had instModuleNNRatOfRat in Mathlib.Algebra.Module.Basic, so for example we could synthesize Module ℚ≥0 ℝ. Is there an obstruction to restoring it?

[Yaël Dillies]

Does

import Mathlib

#synth Module ℚ≥0 ℝ

not work?

[Eric Wieser]

It does not

[Eric Wieser]

Nor does

import Mathlib

variable {F} [Field F] [CharZero F]

#synth Module ℚ≥0 F

[Eric Wieser]

docs#NNRat.instDistribSMul exists

[Eric Wieser]

I think this was probably dropped by accident

[Eric Wieser]

The previous

/-- A `Module` over `ℚ` restricts to a `Module` over `ℚ≥0`. -/
instance [AddCommMonoid α] [Module ℚ α] : Module NNRat α :=
  Module.compHom α NNRat.coeHom

was deleted deliberately, but it seems we forgot to replace it with a new one

[Yaël Dillies]

Ah okay, it must be part of the stuff that I have in APAP but didn't PR yet

[Herman Chau]

Is the intent to replace it with https://github.com/YaelDillies/LeanAPAP/blob/master/LeanAPAP/Mathlib/Algebra/Algebra/Basic.lean#L11-L14?

This came up when I was testing Scott's suggestion for https://github.com/leanprover-community/mathlib4/pull/13585.

[Yaël Dillies]

Yes exactly

[Yaël Dillies]

I can PR it Soon:tm: if you need it

[Herman Chau]

That would be great! I don't need it urgently but would like to merge the PR :smile:

[Yaël Dillies]

@Herman Chau, the PR is #15047