diff options
| author | Cyril Cohen | 2018-02-06 19:36:53 +0100 |
|---|---|---|
| committer | GitHub | 2018-02-06 19:36:53 +0100 |
| commit | d6bc72cd477ed6fe8b95782b26a2e0fc92711395 (patch) | |
| tree | 6996e39182b97573b1cdecaeb7c8c8a3f58c1e77 /mathcomp/real_closed/polyorder.v | |
| parent | 11e539dae1bfe8bc67fc7bd1eb65ee3b4c29f813 (diff) | |
| parent | f3ce9ace4b55654d6240db9eb41a6de3c488f0d9 (diff) | |
Merge pull request #164 from CohenCyril/linting
linting of the whole library
Diffstat (limited to 'mathcomp/real_closed/polyorder.v')
| -rw-r--r-- | mathcomp/real_closed/polyorder.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/real_closed/polyorder.v b/mathcomp/real_closed/polyorder.v index f84abb6..4a96dcc 100644 --- a/mathcomp/real_closed/polyorder.v +++ b/mathcomp/real_closed/polyorder.v @@ -139,9 +139,9 @@ Qed. Lemma mu_mul p q x : p * q != 0 -> \mu_x (p * q) = (\mu_x p + \mu_x q)%N. Proof. -move=>hpqn0; apply/eqP; rewrite eq_sym -muP//. +move=> hpqn0; apply/eqP; rewrite eq_sym -muP//. rewrite exprD dvdp_mul ?root_mu//=. -move:hpqn0; rewrite mulf_eq0 negb_or; case/andP=> hp0 hq0. +move: hpqn0; rewrite mulf_eq0 negb_or; case/andP=> hp0 hq0. move: (mu_spec x hp0)=> [qp qp0 hp]. move: (mu_spec x hq0)=> [qq qq0 hq]. rewrite {2}hp {2}hq exprS exprD !mulrA [qp * _ * _]mulrAC. |