diff options
| author | Yves Bertot | 2020-04-06 14:28:21 +0200 |
|---|---|---|
| committer | GitHub | 2020-04-06 14:28:21 +0200 |
| commit | 80d009e290eb5f935bcd4e341011bc6c5ea61531 (patch) | |
| tree | 9977671907a5afd048943ce7e6eb85db0bbb966d /mathcomp | |
| parent | 0ce6013351c60f0abd4445c9eeccdd3749b071ec (diff) | |
| parent | 942109a5fc1da2f26c58ad13eda095350eb390ff (diff) | |
Merge pull request #472 from affeldt-aist/doc_fix
minor documentation fix
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/solvable/finmodule.v | 3 |
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. |