mathlib4

mathlib4 copied to clipboard

We add Polynomial.nmem_nonZeroDivisors_iff, known as McCoy's theorem: a polynomial P : R[X] is a zerodivisor if and only if there is a : R such that a ≠ 0 and a • P = 0.

• [x] depends on: #12958

Co-authored-by: [email protected]

---

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12958~~ By Dependent Issues (🤖). Happy coding!

maintainer merge

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

I've been hacking on this proof a bit more. I suggest first proving

theorem McCoy (f : R[X]) (h : ∀ r : R, r • f = 0 → r = 0) :
    ∀ (g : R[X]), f * g = 0 → g = 0 := by
  intro g hg
  by_contra hg₀
  have key : ∃ i, g.leadingCoeff * f.coeff i ≠ 0 := by
    contrapose! hg₀
    rw [← leadingCoeff_eq_zero]
    apply h
    simp [Polynomial.ext_iff, hg₀]
  have hnonempty : {i | f.coeff i • g ≠ 0}.Nonempty := key.imp fun i hi ↦ by
    rw [Set.mem_setOf_eq, ← leadingCoeff_ne_zero, smul_eq_C_mul, leadingCoeff_mul']
    all_goals rwa [leadingCoeff_C, mul_comm]
  have hbdd : BddAbove {i | f.coeff i • g ≠ 0} := by
    use f.natDegree
    intro i (hi : f.coeff i • g ≠ 0)
    contrapose! hi
    rw [coeff_eq_zero_of_natDegree_lt hi, zero_smul]
  let m := g.natDegree
  let l := sSup {i | f.coeff i • g ≠ 0}
  have hl : f.coeff l • g ≠ 0 := Nat.sSup_mem hnonempty hbdd
  suffices (f.coeff l • g).natDegree < g.natDegree by
    apply hl
    apply McCoy f h (f.coeff l • g)
    rw [smul_eq_C_mul, mul_left_comm, hg, mul_zero]
  suffices f.coeff l * g.leadingCoeff = 0 by
    apply (natDegree_smul_le (f.coeff l) g).lt_of_ne
    contrapose! hl
    rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]
  suffices (f * g).coeff (l + m) = f.coeff l * g.leadingCoeff by rw [← this, hg, coeff_zero]
  rw [coeff_mul]
  apply Finset.sum_eq_single (l, m) _ (by simp)
  simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]
  intro i j hij H
  obtain hi|rfl|hi := lt_trichotomy i l
  · have hj : m < j := by omega
    rw [coeff_eq_zero_of_natDegree_lt hj, mul_zero]
  · omega
  · suffices f.coeff i • g = 0 by rw [← coeff_C_mul, ← smul_eq_C_mul, this, coeff_zero]
    contrapose! hi
    refine le_csSup hbdd hi
termination_by g => g.natDegree

using recursion.

@jcommelin I've modified the PR using your proof, thanks for the review!

@Ruben-VandeVelde I've reverted your last commit. termination_by does not like variables before the colon.

It feels like the proof of eq_zero_of_mul_eq_zero_of_smul is slightly too complicated, but I can't figure out a way to simplify it (reordering proofs, trying calc blocks, etc.) So looks good to me, thanks!

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style

It feels like the proof of eq_zero_of_mul_eq_zero_of_smul is slightly too complicated, but I can't figure out a way to simplify it (reordering proofs, trying calc blocks, etc.) So looks good to me, thanks!

bors r+

I think the proof is indeed surprisingly tricky! There is a better proof using localization, but it requires a much bigger machinery (and I am not sure it works for semirings...).