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/field/fieldext.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/field/fieldext.v')
| -rw-r--r-- | mathcomp/field/fieldext.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 86d3d39..b8acbd6 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -1311,7 +1311,7 @@ Definition subfx_poly_inv (q : {poly F}) : {poly F} := Let subfx_poly_invE q : iotaPz (subfx_poly_inv q) = (iotaPz q)^-1. Proof. rewrite /subfx_poly_inv. -have [-> | nzq] := altP eqP; first by rewrite rmorph0 invr0. +have [-> | nzq] := eqVneq; first by rewrite rmorph0 invr0. rewrite [nth]lock -[_^-1]mul1r; apply: canRL (mulfK nzq) _; rewrite -rmorphM /=. have rz0: iotaPz (gdcop q p0) = 0. by apply/rootP; rewrite gdcop_map root_gdco ?map_poly_eq0 // p0z0 nzq. |