diff options
| author | Cyril Cohen | 2020-10-30 23:33:53 +0100 |
|---|---|---|
| committer | GitHub | 2020-10-30 23:33:53 +0100 |
| commit | e79b0b06bd3c34735f9dd21c4a705cb9b53da513 (patch) | |
| tree | 372daa93302a212d4e5c6c4923adf582018d00ed | |
| parent | 71f000ff0761cac402074f14fa9fd65d1529fdd5 (diff) | |
| parent | 610eea02513b07386f28d89175382b0f088b6833 (diff) | |
Merge pull request #627 from pi8027/mulpz
Generalize mulpz for any ringType
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 1 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 32 |
2 files changed, 14 insertions, 19 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 29a80db..728476a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -311,6 +311,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - In `srnum.v`, + `>=< y` stands for `[pred x | x >=< y]` +- in `ssrint.v`, generalized `mulpz` for any `ringType`. ### Renamed diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 6d7899b..ca5a5e8 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1708,31 +1708,25 @@ Implicit Types m n : int. Implicit Types i j k : nat. Implicit Types p q r : {poly R}. -Lemma coefMrz : forall p n i, (p *~ n)`_i = (p`_i *~ n). -Proof. by move=> p [] n i; rewrite ?NegzE (coefMNn, coefMn). Qed. +Lemma coefMrz p n i : (p *~ n)`_i = (p`_i *~ n). +Proof. by case: n => n; rewrite ?NegzE (coefMNn, coefMn). Qed. -Lemma polyCMz : forall n, {morph (@polyC R) : c / c *~ n}. -Proof. by case/intP => // n c; rewrite ?mulrNz -!pmulrn ?polyCN ?polyCMn. Qed. +Lemma polyCMz n : {morph (@polyC R) : c / c *~ n}. +Proof. by case: (intP n) => // n' c; rewrite ?mulrNz ?polyCN polyCMn. Qed. -Lemma hornerMz : forall n (p : {poly R}) x, (p *~ n).[x] = p.[x] *~ n. -Proof. by case=> *; rewrite ?NegzE ?mulNzr ?(hornerN, hornerMn). Qed. +Lemma hornerMz n p x : (p *~ n).[x] = p.[x] *~ n. +Proof. by case: n => n; rewrite ?NegzE ?mulNzr ?(hornerN, hornerMn). Qed. -Lemma horner_int : forall n x, (n%:~R : {poly R}).[x] = n%:~R. -Proof. by move=> n x; rewrite hornerMz hornerC. Qed. +Lemma horner_int n x : (n%:~R : {poly R}).[x] = n%:~R. +Proof. by rewrite hornerMz hornerC. Qed. -Lemma derivMz : forall n p, (p *~ n)^`() = p^`() *~ n. -Proof. by move=> [] n p; rewrite ?NegzE -?pmulrn (derivMn, derivMNn). Qed. +Lemma derivMz n p : (p *~ n)^`() = p^`() *~ n. +Proof. by case: n => n; rewrite ?NegzE -?pmulrn (derivMn, derivMNn). Qed. -End PolyZintRing. - -Section PolyZintOIdom. - -Variable R : realDomainType. - -Lemma mulpz (p : {poly R}) (n : int) : p *~ n = n%:~R *: p. -Proof. by rewrite -[p *~ n]mulrzl -mul_polyC polyCMz polyC1. Qed. +Lemma mulpz p n : p *~ n = n%:~R *: p. +Proof. by rewrite -mul_polyC polyCMz polyC1 mulrzl. Qed. -End PolyZintOIdom. +End PolyZintRing. Section ZnatPred. |