degree_prod

Stream: Is there code for X?

[Bolton Bailey]

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]

It seems to only exist for nat_degree, which is the version of degree that doesn't use with_bot.

[Johan Commelin]

$ 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]

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

[Bryan Gin-ge Chen]

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]

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]

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]

You may need to upgrade leanproject. If you installed mathlibtools just using pip then pip install --upgrade mathlibtools should work.

[Yakov Pechersky]

(deleted)

[Bolton Bailey]

(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]

In the meantime, does this work?

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

[Bryan Gin-ge Chen]

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]

pip uninstall mathlibtools ought to remove the version you installed with pip above.

[Bolton Bailey]

@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]

@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]

which leanproject?

[Bolton Bailey]

(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]

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

[Bolton Bailey]

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

[Bolton Bailey]

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]

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

[Bolton Bailey]

Ok, pull request made! #5979