minor documentation fix

1 files changed, 2 insertions, 1 deletions

diff --git a/mathcomp/solvable/finmodule.v b/mathcomp/solvable/finmodule.v
index 05c070e..7920a68 100644
--- a/mathcomp/solvable/finmodule.v
+++ b/mathcomp/solvable/finmodule.v
@@ -38,7 +38,8 @@ From mathcomp Require Import cyclic.
 (* rcosets_cycle_partition), and for any transversal X of HG :* <[g]> the     *)
 (* function r mapping x : gT to rcosets (H :* x) <[g]> is (constructively) a  *)
 (* bijection from X to the <[g]>-orbit partition of HG, and Lemma             *)
-(* transfer_pcycle_def gives a simplified expansion of the transfer morphism. *)
+(* transfer_cycle_expansion gives a simplified expansion of the transfer      *)
+(* morphism.                                                                  *)
 (******************************************************************************)
 
 Set Implicit Arguments.