From 942109a5fc1da2f26c58ad13eda095350eb390ff Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 6 Apr 2020 08:21:41 +0900 Subject: minor documentation fix --- mathcomp/solvable/finmodule.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'mathcomp/solvable/finmodule.v') 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. -- cgit v1.2.3