# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: degree_prod

#### Bolton Bailey (Jan 29 2021 at 07:08):

The file `data/polynomial/degree/definition.lean`

contains a lemma `degree_mul`

for proving that the (with_bot) degree of a product of polynomials is the sum of the degrees of the polynomials. There doesn't seem to be a `degree_prod`

though, for proving that the degree of a finset.prod of polynomials is the finset.sum of the degrees of the polynomials. Does this exist, and if not, can I or someone else add it?

#### Johan Commelin (Jan 29 2021 at 07:25):

It seems to only exist for `nat_degree`

, which is the version of `degree`

that doesn't use `with_bot`

.

#### Johan Commelin (Jan 29 2021 at 07:26):

```
$ rg degree_prod
src/algebra/polynomial/big_operators.lean
18:- `nat_degree_prod_of_monic` : the degree of a product of monic polynomials is the product of
21:- `nat_degree_prod` : for polynomials over an integral domain,
42:lemma nat_degree_prod_le : (∏ i in s, f i).nat_degree ≤ ∑ i in s, (f i).nat_degree :=
71:See `nat_degree_prod` (without the `'`) for a version for integral domains,
74:lemma nat_degree_prod' (h : ∏ i in s, (f i).leading_coeff ≠ 0) :
85:lemma nat_degree_prod_of_monic [nontrivial R] (h : ∀ i ∈ s, (f i).monic) :
88: apply nat_degree_prod',
119: { rw nat_degree_prod_of_monic at h,
124: congr, rw nat_degree_prod_of_monic; { simp [nat_degree_X_sub_C, monic_X_sub_C] },
132:lemma nat_degree_prod (h : ∀ i ∈ s, f i ≠ 0) :
135: apply nat_degree_prod', rw prod_ne_zero_iff,
src/ring_theory/polynomial/cyclotomic.lean
113: rw nat_degree_prod (primitive_roots n R) (λ (z : R), (X - C z)),
src/linear_algebra/char_poly/coeff.lean
70: apply le_trans (polynomial.nat_degree_prod_le univ (λ i : n, (char_matrix M (c i) i))) _,
93: rw nat_degree_prod', simp_rw nat_degree_X_sub_C, unfold fintype.card, simp,
```

#### Johan Commelin (Jan 29 2021 at 07:26):

@Bolton Bailey so yes, feel free to make a PR (-;

#### Bryan Gin-ge Chen (Jan 29 2021 at 07:28):

While looking into this, I just noticed that the doc string for docs#polynomial.nat_degree_prod' had a typo, so I opened a small PR: #5950

#### Eric Wieser (Jan 29 2021 at 09:00):

I'm pretty sure I saw this lemma recently, and it has some extra hypotheses due to how multiplication between top and zero is defined

#### Bolton Bailey (Jan 31 2021 at 01:46):

Seems like it would be fun to try to submit a PR. However, following the instructions here it tells me to run `leanproject get -b mathlib:shiny_lemma`

. Doing this I get the following error.

```
(base) 17:10:07 mathlibcontribution #=# leanproject get -b mathlib:degree_prod
Usage: leanproject get [OPTIONS] NAME [DIRECTORY]
Try 'leanproject get -h' for help.
Error: no such option: -b
```

#### Bryan Gin-ge Chen (Jan 31 2021 at 01:52):

You may need to upgrade `leanproject`

. If you installed `mathlibtools`

just using `pip`

then `pip install --upgrade mathlibtools`

should work.

#### Yakov Pechersky (Jan 31 2021 at 01:55):

(deleted)

#### Bolton Bailey (Jan 31 2021 at 02:05):

```
(base) 17:39:22 mathlibcontribution #=# pip install --upgrade mathlibtools
Collecting mathlibtools
...
Successfully installed PyGithub-1.54.1 deprecated-1.2.11 gitdb-4.0.5 gitpython-3.1.12 mathlibtools-1.0.0 pydot-1.4.1 pyjwt-1.7.1 smmap-3.0.5
(base) 18:00:16 mathlibcontribution #=# leanproject get -b mathlib:degree_prod
Usage: leanproject get [OPTIONS] NAME [DIRECTORY]
Try 'leanproject get -h' for help.
Error: no such option: -b
(base) 18:00:26 mathlibcontribution #=#
```

I guess I didn't install using pip. Is there a way to uninstall leanproject?

#### Yakov Pechersky (Jan 31 2021 at 02:08):

In the meantime, does this work?

```
leanproject get leanprover-community/mathlib
cd mathlib
leanproject pr degree_prod
```

#### Bryan Gin-ge Chen (Jan 31 2021 at 02:09):

Maybe you installed it via `pipx`

? If so, then `pipx upgrade mathlibtools`

should work. I'm assuming you followed the instructions here for a certain OS?

#### Bryan Gin-ge Chen (Jan 31 2021 at 02:09):

`pip uninstall mathlibtools`

ought to remove the version you installed with `pip`

above.

#### Bolton Bailey (Jan 31 2021 at 02:11):

@Eric Wieser There is a lemma `lemma degree_mul : degree (p * q) = degree p + degree q`

without any additional hypotheses, (which is indeed strange to me because I think it means `0 + \bot`

must be defined as `\bot`

, which contradicts the usual zero as additive identity).

#### Bolton Bailey (Jan 31 2021 at 02:12):

@Yakov Pechersky my leanproject has no pr command. I have

```
Usage: leanproject [OPTIONS] COMMAND [ARGS]...
Try 'leanproject -h' for help.
Error: No such command 'pr'.
(base) 18:09:49 mathlib #=# leanproject --version
leanproject, version 0.0.5
```

#### Yakov Pechersky (Jan 31 2021 at 02:13):

`which leanproject`

?

#### Bolton Bailey (Jan 31 2021 at 02:15):

```
(base) 18:09:59 mathlib #=# which leanproject
/Library/Frameworks/Python.framework/Versions/3.8/bin/leanproject
(base) 18:14:58 mathlib #=# python --version
Python 3.7.6
```

#### Bolton Bailey (Jan 31 2021 at 02:17):

Perhaps I just need to pip upgrade in the right conda environment, one sec

#### Bolton Bailey (Jan 31 2021 at 02:21):

Ok, yep, that was the issue, I am now on leanproject 1.0.0, thanks all for your help

#### Bolton Bailey (Jan 31 2021 at 05:04):

Ok, I have made an implementation for this

```
section nontrivial_no_zero_divisors
variables [comm_semiring R] [nontrivial R] [no_zero_divisors R] (f : ι → polynomial R)
/--
The degree of a product of polynomials is equal to
the sum of the degrees, where the degree of the zero polynomial is ⊥.
-/
lemma degree_prod : (∏ i in s, f i).degree = ∑ i in s, (f i).degree :=
begin
classical,
induction s using finset.induction with a s ha hs, { simp },
rw [prod_insert ha, sum_insert ha],
rw polynomial.degree_mul, rw hs,
end
end nontrivial_no_zero_divisors
```

The contribution guide says I should ask for non-master branch write access. My github username is BoltonBailey. Can I have access?

#### Bryan Gin-ge Chen (Jan 31 2021 at 05:07):

@Bolton Bailey Invite sent! https://github.com/leanprover-community/mathlib/invitations

#### Bolton Bailey (Jan 31 2021 at 07:30):

Ok, pull request made! #5979

Last updated: May 16 2021 at 05:21 UTC