diff options
| author | Enrico | 2017-08-13 13:53:43 +0200 |
|---|---|---|
| committer | GitHub | 2017-08-13 13:53:43 +0200 |
| commit | ed467b353b040f1a87ba7ce3242d28bc9423acbb (patch) | |
| tree | 33f0cde957e5322583d27b01345fe27490732d19 | |
| parent | 8cc0b96f21dbc3818a0c5dfd778d9cadd66e4beb (diff) | |
| parent | 73c1848f2678e03e8bda249413a081c498d58e62 (diff) | |
Merge pull request #134 from PatrickMassot/master
Fix typo in fingroup documentation
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 550aaaa..06a1806 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -130,7 +130,7 @@ Require Import div path bigop prime finset. (* In addition to the generic suffixes described in ssrbool.v and finset.v, *) (* we associate the following suffixes to group operations: *) (* 1 - identity element, as in group1 : 1 \in G. *) -(* M - multiplication, as is invMg : (x * y)^-1 = x^-1 * y^-1. *) +(* M - multiplication, as is invMg : (x * y)^-1 = y^-1 * x^-1. *) (* Also nat multiplication, for expgM : x ^+ (m * n) = x ^+ m ^+ n. *) (* D - (nat) addition, for expgD : x ^+ (m + n) = x ^+ m * x ^+ n. *) (* V - inverse, as in mulgV : x * x^-1 = 1. *) |