module has_scalar

Stream: new members

[Kalle Kytölä]

I have some trouble inferring has_scalar from module.

As far as I can see, docs#module extends docs#distrib_mul_action, which extends docs#mul_action, which extends docs#has_scalar. Nevertheless, assuming module, I fail to apply_instance to get a has_scalar:

import algebra.algebra.basic

variables (E : Type*) [add_comm_group E]
def foo₁ : has_add E := by apply_instance -- works

variables (𝕜 : Type*) [semiring 𝕜] [module 𝕜 E]
def foo₂ : has_scalar E 𝕜 := by apply_instance -- fails (error message below)

/-
tactic.mk_instance failed to generate instance for
  has_scalar E 𝕜
state:
E : Type u_1,
_inst_1 : add_comm_group E,
𝕜 : Type u_2,
_inst_2 : semiring 𝕜,
_inst_3 : module 𝕜 E
⊢ has_scalar E 𝕜
-/

What am I doing wrong? :speechless: Thanks in advance!

[Kalle Kytölä]

Oh no, nevermind... I just got the arguments in the wrong order!

The following is fine:

import algebra.algebra.basic

variables (E : Type*) [add_comm_group E]
def foo₁ : has_add E := by apply_instance -- works
variables (𝕜 : Type*) [semiring 𝕜] [module 𝕜 E]
def foo₃ : has_scalar 𝕜 E := by apply_instance -- works

[Kalle Kytölä]

(For some reason I thought the M argument should be the "module", and not the "monoid" of scalars... :face_palm:)