diff options
| author | Cyril Cohen | 2017-11-23 16:33:36 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2018-02-06 13:54:37 +0100 |
| commit | fafd4dac5315e1d4e071b0044a50a16360b31964 (patch) | |
| tree | 5b66c3d67e2b146e3a8013496379b96dd60dc75a /mathcomp/real_closed/polyorder.v | |
| parent | 835467324db450c8fb8971e477cc4d82fa3e861b (diff) | |
running semi-automated linting on 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. |