diff options
| author | Kazuhiko Sakaguchi | 2020-10-09 00:21:00 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-10-29 12:31:31 +0900 |
| commit | c6e0d703165b0c60c270672eb542aa8934929bfe (patch) | |
| tree | 3ce1b05b861ca60e88bc7ab8b5226b12a879e3e6 /mathcomp/fingroup | |
| parent | fe8759d1faec24cbe9d838f777682e260680d370 (diff) | |
Switch from long suffixes to short suffixes
Diffstat (limited to 'mathcomp/fingroup')
| -rw-r--r-- | mathcomp/fingroup/gproduct.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 7e14ce0..cdd68fd 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -829,7 +829,7 @@ have{defGi} defGi: \big[dprod/1]_(j | Q j && (j != i)) A j = Gi. by apply: IHm => [||j /andP[/sQP]] //; rewrite (cardD1x Qi) in leQm. rewrite defGi dprodE // coprime_TIg // -defAi -(bigdprod_card defGi). elim/big_rec: _ => [|j n /andP[neq_ji Qj] IHn]; first exact: coprimen1. -by rewrite coprime_mulr coprime_sym coA ?sQP. +by rewrite coprimeMr coprime_sym coA ?sQP. Qed. Lemma mem_dprod G A B x : A \x B = G -> x \in G -> |