Annihilator of modules over noncommutative ring

Stream: new members

[Haruhisa Enomoto]

Sorry again for my noncomutative question.
I encountered the problem (for me) that an annihilator of a module over a ring is only defined for commutative rings in submodule.annihilator.
I want it to work for noncommutative rings, but some problem arises.
In mathlib, annihilator of M is defined to be the kernel of left action, which is R-hom, so it automatically becomes an left ideal. But the same definition doesn't work for noncommutative case.
I think the solution of this is to

1. change the definition of submodule.annihilator to include the noncommutative case, and
2. rewrite all the proof which use submodule.annihilator.

Is this a correct way? Or maybe is there any simple solution?
(And I also wonder how to define submodule.annihilator so that part 2 becomes easier.)

[Johan Commelin]

I think you could do (1), and then add a lemma submodule.annihilator_def_cr which proves that it is the same as the old def in the commutative case. After that (2) should be easy (just rw with that new lemma, when needed).

[Johan Commelin]

Once that is done, you can generalize the rest of the API to the nc case in bits and pieces as needed.

[Eric Wieser]

I would guess we want a version of linear_map.lsmul with a right action by R somewhere?