[Merged by Bors] - feat: Lemmas for some monomial orders by AntoineChambert-Loir · Pull Request #16177 · leanprover-community/mathlib4

AntoineChambert-Loir · 2024-08-27T10:21:58Z

This is a PR of technical lemmas relative to monomial orders and polynomials that were taken out of the formalization of Alon's Combinatorial Nullstellensatz which now belongs to #20495

degree of a product for the deglex monomial order, multiplicativity of the leading coefficients
degree (for a monomial order) of monomials
the leading coefficient (for a monomial order) of a nonzero polynomial is nonzero.

depends on: [Merged by Bors] - chore(RingTheory/MvPolynomial/WeightedHomogeneous): golf the proof a lemma #20697
depends on: [Merged by Bors] - feat(Data/Finsupp/MonomialOrder) : lexicographic order on Unique #20699
depends on: [Merged by Bors] - feat(Data/Finsupp/MonomialOrder): monomial orders #19453
depends on: [Merged by Bors] - feat(RingTheory/MvPolynomial/Groebner): division algorithm wrt monomial orders #19454
depends on: [Merged by Bors] - feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order #19455
depends on: [Merged by Bors] - chore(Mathlib/RingTheory/MvPolynomial): rename MonomialOrder.lCoeff to MonomialOrder.leadingCoeff #21290

Two other enhancements are delegated to two other PRs on which this one now depends.

github-actions · 2024-08-27T10:22:40Z

PR summary 0f2bb639d4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex` (new file)	1140

Declarations diff

+ coeff_mul_of_add_of_degree_le
+ coeff_prod_sum_degree
+ degLex_totalDegree_monotone
+ degree_X
+ degree_X_le_single
+ degree_degLexDegree
+ degree_prod
+ degree_prod_le
+ degree_prod_of_regular
+ leadingCoeff_prod_of_regular

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

github-actions

Remaining comments which cannot be posted as a review comment to avoid GitHub Rate Limit

lint-style

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 381 in b2327b3

theorem eq_zero_of_eval_zero_at_prod_nat {n : ℕ} [IsDomain R]

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 383 to 388 in b2327b3

    
             (Hdeg : ∀ i, P.weightedTotalDegree (Finsupp.single i 1) < (S i).ncard)  
        
             (Heval : ∀ (x : Fin n → R), (∀ i, x i ∈ S i) → eval x P = 0) :  
        
             P = 0 := by  
        
           induction n generalizing R with  
        
           | zero =>  
        
             suffices P = C (constantCoeff P) by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 392 in b2327b3

ext m

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 397 in b2327b3

| succ n hrec =>

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 399 in b2327b3

suffices Q = 0 by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 402 to 403 in b2327b3

    
           have Heval' : ∀ (x : Fin n → R) (_ : ∀ i, x i ∈ S i.succ),  
        
             Polynomial.map (eval x) Q = 0 := fun x hx ↦ by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 422 in b2327b3

· intro z _ hz

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 424 in b2327b3

· simp

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 428 in b2327b3

intro i

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 460 in b2327b3

    
           noncomputable example (s : R) : Polynomial R := Polynomial.X (R := R) - Polynomial.C s

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 462 in b2327b3

noncomputable example (S : Finset R) : Polynomial R :=

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 476 in b2327b3

intro m hm

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 511 in b2327b3

rintro ⟨u, v⟩ h

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 520 to 521 in b2327b3

    
           lemma prod_support_le {ι : Type*} (i : ι) (s : Finset R) (m : ι →₀ ℕ)  
        
               (hm : m ∈ (s.prod (fun r ↦ X i - C r)).support) :

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 525 in b2327b3

| empty =>

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 532 in b2327b3

| @insert a s has h =>

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 607 in b2327b3

have hf : f = f' + monomial d (f.coeff d) := by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 609 in b2327b3

have hf' : f'.support = f.support.erase d := by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 623 in b2327b3

obtain ⟨h', r', Hf', Hh', Hr'⟩ := hrec f' hf'D

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 644 in b2327b3

rw [← ne_eq, ← mem_support_iff]

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 659 in b2327b3

-- write `monomial d (f.coeff d) = `monomial d' (f.coeff d) * _ + f''`

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 662 in b2327b3

have hf'' : monomial d (f.coeff d)

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 686 in b2327b3

by_cases h' : d' ≤ b

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 716 in b2327b3

simp only [Finset.mem_antidiagonal]

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 742 in b2327b3

obtain ⟨h'', r'', Hf'', Hh'', Hr''⟩ := hrec f'' hf''2

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 766 in b2327b3

· intro h

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 789 in b2327b3

· simp

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 796 in b2327b3

    
           (f : MvPolynomial (Fin n) R) (Heval : ∀ (x : Fin n → R), (∀ i, x i ∈ S i) → eval x f = 0) :

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 803 in b2327b3

apply eq_zero_of_eval_zero_at_prod_nat r (fun i ↦ S i)

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 818 to 822 in b2327b3

    
           theorem Alon2 {n : ℕ} [IsDomain R]  
        
               (f : MvPolynomial (Fin n) R)  
        
               (t : Fin n →₀ ℕ) (ht : f.coeff t ≠ 0) (ht' : f.totalDegree = t.degree)  
        
               (S : Fin n → Finset R) (htS : ∀ i, t i < (S i).card) :  
        
               ∃ (s : Fin n → R) (_ : ∀ i, s i ∈ S i), eval s f ≠ 0 := by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 826 to 827 in b2327b3

    
           obtain ⟨h, hh, hf⟩ := Alon1 S  
        
             (fun i ↦ by rw [← Finset.card_pos]; exact lt_of_le_of_lt (zero_le _) (htS i))

github-actions

Remaining comments which cannot be posted as a review comment to avoid GitHub Rate Limit

lint-style

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 386 in 244d91a

theorem eq_zero_of_eval_zero_at_prod_nat {n : ℕ} [IsDomain R]

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 388 to 393 in 244d91a

    
             (Hdeg : ∀ i, P.weightedTotalDegree (Finsupp.single i 1) < (S i).ncard)  
        
             (Heval : ∀ (x : Fin n → R), (∀ i, x i ∈ S i) → eval x P = 0) :  
        
             P = 0 := by  
        
           induction n generalizing R with  
        
           | zero =>  
        
             suffices P = C (constantCoeff P) by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 397 in 244d91a

ext m

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 402 in 244d91a

| succ n hrec =>

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 404 in 244d91a

suffices Q = 0 by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 407 to 408 in 244d91a

    
           have Heval' : ∀ (x : Fin n → R) (_ : ∀ i, x i ∈ S i.succ),  
        
             Polynomial.map (eval x) Q = 0 := fun x hx ↦ by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 427 in 244d91a

· intro z _ hz

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 429 in 244d91a

· simp

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 433 in 244d91a

intro i

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 465 in 244d91a

    
           noncomputable example (s : R) : Polynomial R := Polynomial.X (R := R) - Polynomial.C s

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 467 in 244d91a

noncomputable example (S : Finset R) : Polynomial R :=

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 481 in 244d91a

intro m hm

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 516 in 244d91a

rintro ⟨u, v⟩ h

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 525 to 526 in 244d91a

    
           lemma prod_support_le {ι : Type*} (i : ι) (s : Finset R) (m : ι →₀ ℕ)  
        
               (hm : m ∈ (s.prod (fun r ↦ X i - C r)).support) :

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 530 in 244d91a

| empty =>

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 537 in 244d91a

| @insert a s has h =>

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 612 in 244d91a

have hf : f = f' + monomial d (f.coeff d) := by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 614 in 244d91a

have hf' : f'.support = f.support.erase d := by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 628 in 244d91a

obtain ⟨h', r', Hf', Hh', Hr'⟩ := hrec f' hf'D

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 649 in 244d91a

rw [← ne_eq, ← mem_support_iff]

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 664 in 244d91a

-- write `monomial d (f.coeff d) = `monomial d' (f.coeff d) * _ + f''`

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 667 in 244d91a

have hf'' : monomial d (f.coeff d)

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 691 in 244d91a

by_cases h' : d' ≤ b

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 721 in 244d91a

simp only [Finset.mem_antidiagonal]

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 747 in 244d91a

obtain ⟨h'', r'', Hf'', Hh'', Hr''⟩ := hrec f'' hf''2

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 771 in 244d91a

· intro h

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 794 in 244d91a

· simp

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 801 in 244d91a

    
           (f : MvPolynomial (Fin n) R) (Heval : ∀ (x : Fin n → R), (∀ i, x i ∈ S i) → eval x f = 0) :

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 808 in 244d91a

apply eq_zero_of_eval_zero_at_prod_nat r (fun i ↦ S i)

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 823 to 827 in 244d91a

    
           theorem Alon2 {n : ℕ} [IsDomain R]  
        
               (f : MvPolynomial (Fin n) R)  
        
               (t : Fin n →₀ ℕ) (ht : f.coeff t ≠ 0) (ht' : f.totalDegree = t.degree)  
        
               (S : Fin n → Finset R) (htS : ∀ i, t i < (S i).card) :  
        
               ∃ (s : Fin n → R) (_ : ∀ i, s i ∈ S i), eval s f ≠ 0 := by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 831 to 832 in 244d91a

    
           obtain ⟨h, hh, hf⟩ := Alon1 S  
        
             (fun i ↦ by rw [← Finset.card_pos]; exact lt_of_le_of_lt (zero_le _) (htS i))

github-actions

Remaining comments which cannot be posted as a review comment to avoid GitHub Rate Limit

lint-style

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 832 in 74b2d05

· simp

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 839 in 74b2d05

    
           /- theorem euclDivd {n : ℕ} (S : Fin n → Finset R) (Sne : ∀ i, (S i).Nonempty)

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 866 in 74b2d05

have hf : f = f' + monomial d (f.coeff d) := by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 868 in 74b2d05

have hf' : f'.support = f.support.erase d := by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 882 in 74b2d05

obtain ⟨h', r', Hf', Hh', Hr'⟩ := hrec f' hf'D

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 903 in 74b2d05

rw [← ne_eq, ← mem_support_iff]

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 918 in 74b2d05

-- write `monomial d (f.coeff d) = `monomial d' (f.coeff d) * _ + f''`

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 921 in 74b2d05

have hf'' : monomial d (f.coeff d)

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 945 in 74b2d05

by_cases h' : d' ≤ b

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 975 in 74b2d05

simp only [Finset.mem_antidiagonal]

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 1001 in 74b2d05

obtain ⟨h'', r'', Hf'', Hh'', Hr''⟩ := hrec f'' hf''2

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 1025 in 74b2d05

· intro h

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 1048 in 74b2d05

· simp

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 1056 in 74b2d05

    
           (f : MvPolynomial σ R) (Heval : ∀ (x : σ → R), (∀ i, x i ∈ S i) → eval x f = 0) :

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Line 1063 in 74b2d05

apply eq_zero_of_eval_zero_at_prod r (fun i ↦ S i)

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 1078 to 1082 in 74b2d05

    
           theorem Alon2 [IsDomain R]  
        
               (f : MvPolynomial σ R)  
        
               (t : σ →₀ ℕ) (ht : f.coeff t ≠ 0) (ht' : f.totalDegree = t.degree)  
        
               (S : σ → Finset R) (htS : ∀ i, t i < (S i).card) :  
        
               ∃ (s : σ → R) (_ : ∀ i, s i ∈ S i), eval s f ≠ 0 := by

[lint-style] _{reported by reviewdog 🐶}

mathlib4/Mathlib/Combinatorics/Nullstellensatz.lean

Lines 1087 to 1088 in 74b2d05

    
           obtain ⟨h, hh, hf⟩ := Alon1 S  
        
             (fun i ↦ by rw [← Finset.card_pos]; exact lt_of_le_of_lt (zero_le _) (htS i))

Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

mathlib4-dependent-issues-bot · 2025-01-31T19:49:26Z

This PR/issue depends on:

~~[Merged by Bors] - chore(RingTheory/MvPolynomial/WeightedHomogeneous): golf the proof a lemma #20697~~
~~[Merged by Bors] - feat(Data/Finsupp/MonomialOrder) : lexicographic order on Unique #20699~~
~~[Merged by Bors] - feat(Data/Finsupp/MonomialOrder): monomial orders #19453~~
~~[Merged by Bors] - feat(RingTheory/MvPolynomial/Groebner): division algorithm wrt monomial orders #19454~~
~~[Merged by Bors] - feat(Data/Finsupp/MonomialOrder/DegLex): homogeneous lexicographic order #19455~~
~~[Merged by Bors] - chore(Mathlib/RingTheory/MvPolynomial): rename MonomialOrder.lCoeff to MonomialOrder.leadingCoeff #21290~~
By Dependent Issues (🤖). Happy coding!

YaelDillies

Thanks!

maintainer delegate

Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean

github-actions · 2025-01-31T20:12:46Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

jcommelin

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

mathlib-bors · 2025-01-31T20:32:38Z

✌️ AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

AntoineChambert-Loir · 2025-01-31T20:52:26Z

bors r+

This is a PR of technical lemmas relative to monomial orders and polynomials that were taken out of the formalization of Alon's Combinatorial Nullstellensatz which now belongs to #20495 * degree of a product for the deglex monomial order, multiplicativity of the leading coefficients * degree (for a monomial order) of monomials * the leading coefficient (for a monomial order) of a nonzero polynomial is nonzero.

mathlib-bors · 2025-01-31T21:02:24Z

Pull request successfully merged into master.

Build succeeded:

* factorial-dvd-int: (143 commits) Apply suggestions from code review feat(Factorial): k! divides the product of any k successive integers feat(CategoryTheory): creation of finite limits (#21320) chore: update Mathlib dependencies 2025-02-01 (#21328) chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314) feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306) chore: cleanup imports in Archive/IfNormalization (#21318) doc: fix several typos (#21315) feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310) chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271) feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084) chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308) feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522) feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168) chore: update Mathlib dependencies 2025-02-01 (#21312) chore: update Mathlib dependencies 2025-01-31 (#21311) feat: generalize `mem_dite` to `Membership α β` (#21262) feat: Lemmas for some monomial orders (#16177) feat(CategoryTheory): the localized category is monoidal (#12728) feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295) feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284) fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299) feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199) refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653) feat(RingTheory/PowerSeries): binomial series (#20192) chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff (#21290) chore (RingTheory/HahnSeries): fix names that use coeff (#21279) feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233) chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273) feat(CategoryTheory): the monoidal category structure on a localization (#20951) feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009) feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328) feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486) feat: Function.const as a PartialEquiv (#21137) chore(NonZeroDivisors): don't import rings (#20871) feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267) feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190) feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285) perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179) feat(Order): order isomorphisms from `Fin n` for small `n` (#21120) refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740) feat: Sylow's first theorem for elementary `p`-groups (#21072) chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748) refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213) feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186) feat(Algebra/Group/Action): add definition of equidecomposition (#16936) feat(CategoryTheory/Subpresheaf): equalizer (#21096) feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204) chore: update Mathlib dependencies 2025-01-31 (#21282) ...

This is a PR of technical lemmas relative to monomial orders and polynomials that were taken out of the formalization of Alon's Combinatorial Nullstellensatz which now belongs to #20495 * degree of a product for the deglex monomial order, multiplicativity of the leading coefficients * degree (for a monomial order) of monomials * the leading coefficient (for a monomial order) of a nonzero polynomial is nonzero.

AntoineChambert-Loir added 10 commits August 18, 2024 03:22

initial commit

dd41a2c

add docstring

5839a85

progress

4f3169c

small progress

e490d4f

start defining linear order

c46fff9

prob. ok pour la multiplication

37feb31

presque rien

94f83d0

big progress

ce26f63

Alon's First Combinatorial Nullstellensatz

434d61b

full proof of Combinatorial Nullstellensatz

b2327b3

github-actions bot reviewed Aug 27, 2024

View reviewed changes

fix lint style

244d91a

github-actions bot reviewed Aug 27, 2024

View reviewed changes

grunweg changed the title ~~Feat(Mathlib/Combinatorics/Nullstellensatz) : Alon's Combinatorial Nullstellensatz~~ feat(Mathlib/Combinatorics/Nullstellensatz) : Alon's Combinatorial Nullstellensatz Aug 27, 2024

grunweg added the t-combinatorics Combinatorics label Aug 27, 2024

make it work for finite types

74b2d05

github-actions bot reviewed Aug 30, 2024

View reviewed changes

AntoineChambert-Loir added 12 commits August 30, 2024 19:18

lint-style

eaca76d

try to have euclDivd work recursively

57063ff

lint-style

7beb580

initial commit

e79b5ca

starting

b9e1875

apply zuggestions from Giacomo Stevanato

a8ff2b1

lint-style

ef9bb5e

some progress

e0c6b4f

lint-style

a76a105

progress

27d6b7d

euclidean division for a monomial order

ac438fd

division algorithm

e9beb33

AntoineChambert-Loir added 4 commits January 31, 2025 09:26

rename lCoeff to leadingCoeff

c801df8

follow YD's suggestions minus an unresolved question

5fb9596

adjust lCoeff to leadingCoeff

3f9b138

delete lemmas for subsingleton

11205fc

AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 31, 2025

YaelDillies reviewed Jan 31, 2025

View reviewed changes

Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean Show resolved Hide resolved

mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jan 31, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 31, 2025

merge master

8ae4248

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 31, 2025

YaelDillies approved these changes Jan 31, 2025

View reviewed changes

Mathlib/RingTheory/MvPolynomial/MonomialOrder/DegLex.lean Outdated Show resolved Hide resolved

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 31, 2025

AntoineChambert-Loir added 3 commits January 31, 2025 21:21

mv hypotheses to variable

71f8b36

adjust to bad merge

3e67b87

it\'s time to stop

0f2bb63

jcommelin reviewed Jan 31, 2025

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 31, 2025

mathlib-bors bot changed the title ~~feat: Lemmas for some monomial orders~~ [Merged by Bors] - feat: Lemmas for some monomial orders Jan 31, 2025

mathlib-bors bot closed this Jan 31, 2025

mathlib-bors bot deleted the ACL/CombNS branch January 31, 2025 21:02

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: Lemmas for some monomial orders#16177

[Merged by Bors] - feat: Lemmas for some monomial orders#16177
AntoineChambert-Loir wants to merge 126 commits intomasterfrom
ACL/CombNS

AntoineChambert-Loir commented Aug 27, 2024 •

edited by YaelDillies

Loading

Uh oh!

github-actions bot commented Aug 27, 2024 •

edited

Loading

Declarations diff

Uh oh!

github-actions bot left a comment

Uh oh!

github-actions bot left a comment

Uh oh!

github-actions bot left a comment

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Jan 31, 2025

Uh oh!

YaelDillies left a comment

Uh oh!

Uh oh!

github-actions bot commented Jan 31, 2025

Uh oh!

jcommelin left a comment

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

AntoineChambert-Loir commented Jan 31, 2025

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

	(Hdeg : ∀ i, P.weightedTotalDegree (Finsupp.single i 1) < (S i).ncard)
	(Heval : ∀ (x : Fin n → R), (∀ i, x i ∈ S i) → eval x P = 0) :
	P = 0 := by
	induction n generalizing R with
	\| zero =>
	suffices P = C (constantCoeff P) by

	have Heval' : ∀ (x : Fin n → R) (_ : ∀ i, x i ∈ S i.succ),
	Polynomial.map (eval x) Q = 0 := fun x hx ↦ by

	lemma prod_support_le {ι : Type*} (i : ι) (s : Finset R) (m : ι →₀ ℕ)
	(hm : m ∈ (s.prod (fun r ↦ X i - C r)).support) :

	theorem Alon2 {n : ℕ} [IsDomain R]
	(f : MvPolynomial (Fin n) R)
	(t : Fin n →₀ ℕ) (ht : f.coeff t ≠ 0) (ht' : f.totalDegree = t.degree)
	(S : Fin n → Finset R) (htS : ∀ i, t i < (S i).card) :
	∃ (s : Fin n → R) (_ : ∀ i, s i ∈ S i), eval s f ≠ 0 := by

	obtain ⟨h, hh, hf⟩ := Alon1 S
	(fun i ↦ by rw [← Finset.card_pos]; exact lt_of_le_of_lt (zero_le _) (htS i))

	theorem Alon2 [IsDomain R]
	(f : MvPolynomial σ R)
	(t : σ →₀ ℕ) (ht : f.coeff t ≠ 0) (ht' : f.totalDegree = t.degree)
	(S : σ → Finset R) (htS : ∀ i, t i < (S i).card) :
	∃ (s : σ → R) (_ : ∀ i, s i ∈ S i), eval s f ≠ 0 := by

Conversation

AntoineChambert-Loir commented Aug 27, 2024 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Aug 27, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 0f2bb639d4

Import changes for modified files

Declarations diff

Uh oh!

github-actions bot left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Jan 31, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Jan 31, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

AntoineChambert-Loir commented Jan 31, 2025

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

AntoineChambert-Loir commented Aug 27, 2024 •

edited by YaelDillies

Loading

github-actions bot commented Aug 27, 2024 •

edited

Loading