naming: lie_smul

Stream: maths

[Johan Commelin]

Currently, in mathlib, we have

@[simp] lemma lie_smul  (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L]
  (t : R) (x y : L) : ⁅x, t • y⁆ = t • ⁅x, y⁆ :=
 lie_algebra.lie_smul t x y

However, if we want to define a lie_action (which will be part of lie_module), then this is one of the axioms
image.png
which I assume would be called lie_smul.

Does anyone have a good suggestion for fixing this naming conflict?
The best I have come up with is a namespaced lie_action.lie_smul. But that's quite a mouthful.

[Eric Wieser]

Should the existing one be lie_smul_right, to distinguish from the case with t . x, y?

[Johan Commelin]

No, the latter would be smul_lie...

[Johan Commelin]

... in the current naming scheme.

[Johan Commelin]

But I guess we need a more sophisticated naming scheme to distinguish all the possible combinations

[Eric Wieser]

I thought the naming was assuming all functions were prefix notation

[Eric Wieser]

Ah I guess add_mul vs mul_add is the counterexample I need

[Kenny Lau]

@Johan Commelin the second one is called lie_smul', the third one lie_smul'', etc.

[Kenny Lau]

(/s)

[Oliver Nash]

@Johan Commelin am I confused or do we not already have a version of this here ?

[Oliver Nash]

(called lie_act)

[Oliver Nash]

(As it happens I have plans to refactor lie_module in my non-existent copious free time so that the action is an instance of has_scalar.)

[Johan Commelin]

@Oliver Nash Oooh cool! I didn't realise we already had this!

[Johan Commelin]

Thanks for the pointer

[Oliver Nash]

Let me know if there’s anything I can do to help. Perhaps I should just bump the priority of that refactor I mentioned?

[Johan Commelin]

@Oliver Nash If such a priority bumping feature is available... I would happily see the results :grinning: