diff options
| author | Cyril Cohen | 2020-01-03 14:45:53 +0100 |
|---|---|---|
| committer | GitHub | 2020-01-03 14:45:53 +0100 |
| commit | c7fa2a1444d450bcebdeea47800fef1436690b6d (patch) | |
| tree | e0cf42c9b4b8ad39ddec274a368e1f6800b9cc49 /mathcomp/solvable/cyclic.v | |
| parent | a93a392121e8e02c6fdaa6c674dd90af8b12c28d (diff) | |
| parent | a06d61a8e226eeabc52f1a22e469dca1e6077065 (diff) | |
Merge pull request #443 from pi8027/eqVneq
Refactoring and linting proofs especially in polydiv.v
Diffstat (limited to 'mathcomp/solvable/cyclic.v')
| -rw-r--r-- | mathcomp/solvable/cyclic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index e6d3afb..d82009b 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -587,7 +587,7 @@ Variable u : {unit 'Z_#[a]}. Lemma injm_cyclem : 'injm (cyclem (val u) a). Proof. apply/subsetP=> x /setIdP[ax]; rewrite !inE -order_dvdn. -case: (eqVneq a 1) => [a1 | nta]; first by rewrite a1 cycle1 inE in ax. +have [a1 | nta] := eqVneq a 1; first by rewrite a1 cycle1 inE in ax. rewrite -order_eq1 -dvdn1; move/eqnP: (valP u) => /= <-. by rewrite dvdn_gcd {2}Zp_cast ?order_gt1 // order_dvdG. Qed. @@ -616,7 +616,7 @@ Canonical Zp_unit_morphism := Morphism Zp_unitmM. Lemma injm_Zp_unitm : 'injm Zp_unitm. Proof. -case: (eqVneq a 1) => [a1 | nta]. +have [a1 | nta] := eqVneq a 1. by rewrite subIset //= card_le1_trivg ?subxx // card_units_Zp a1 order1. apply/subsetP=> /= u /morphpreP[_ /set1P/= um1]. have{um1}: Zp_unitm u a == Zp_unitm 1 a by rewrite um1 morph1. |