Zulip Chat Archive

Stream: Is there code for X?

Topic: degree_prod


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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,

view this post on Zulip Johan Commelin (Jan 29 2021 at 07:26):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Jan 31 2021 at 01:55):

(deleted)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Jan 31 2021 at 02:09):

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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jan 31 2021 at 02:13):

which leanproject?

view this post on Zulip 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

view this post on Zulip Bolton Bailey (Jan 31 2021 at 02:17):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Jan 31 2021 at 05:07):

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

view this post on Zulip Bolton Bailey (Jan 31 2021 at 07:30):

Ok, pull request made! #5979


Last updated: May 16 2021 at 05:21 UTC