Kazuhiko Sakaguchi

@affeldt-aist Is this the meeting you're referring to? It doesn't even say we decided to rename `GRing.exp` to `pown`: https://github.com/math-comp/math-comp/wiki/Minutes-2024-09-04

IMO, the following definitions should ideally follow the same naming pattern, with no ambiguity/naming conflict: - `Algebra.natmul` in `nmodule.v` (= `GRing.natmul` in `ssralg.v`), - `natexp` in `monoid.v` (= `expgn` in...

I also argue that renaming `GRing.exp` to `GRing.pown` is a bad idea, while `GRing.pow*r*n` might be acceptable, because we may eventually want to rename `expn` to `pown`.

I agree that my proposal goes beyond what we usually do in a single PR. I think that renaming `GRing.exp` to `GRing.exprn` (optionally `natexp` to `expgz`) and some lemmas is...

I suggest waiting for some input from others before starting any implementation work. @Tragicus @CohenCyril @proux01

@CohenCyril Right. I didn't see the issues before reading the patch. @affeldt-aist Just in case, let me write down the naming convention I suggest here, so that we can discuss...

@affeldt-aist But there already are `order/order.v`, `fingroup/fingroup.v`, and `character/character.v`, and I'm about to introduce `algebra.v` in #1504.

If we decide to introduce such a file, it should probably provide an overview of the directory. So this is also a question of documentation.

We discussed this issue during the [MathComp meeting](https://github.com/math-comp/math-comp/wiki/Minutes-2025-12-10). The consensus was to introduce `all_.v`, e.g., `all_num_theory.v` and `all_alg_theory.v`, but we may want to remove `_theory` from both directory name and...

To be clear, I will neither further review this PR nor maintain this code. I suggest finding another reviewer who can potentially co-maintain the code.