PR summary 78720593bd

Import changes for modified files

No significant changes to the import graph

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

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

This PR/issue depends on:

• [Merged by Bors] - feat: add LinearMap.IsAlt.eq_of_add_add_eq_zero #14281
  By Dependent Issues (🤖). Happy coding!

@eric-wieser Could you help me for setup? I'm trying to understand how the BilinForm works and how to adapt it to Wronskian. In fact, I cannot figure out how to "state" the theorem wronskianBilin. I found that the core definition of BilinForm is defined as mk₂ in LinearAlgebra/BilinearMap.lean, but not sure where to start. For example, do I need to re-write the definition of current Wronskian? Once I figure out the statements, I think I can prove it myself.

With

import Mathlib.Algebra.Polynomial.AlgebraMap
import Mathlib.LinearAlgebra.SesquilinearForm
import Mathlib.Algebra.Algebra.Bilinear

you can write

variable (R) in
/-- `Polynomial.wronskian` as a bilinear map. -/
def wronskianBilin : R[X] →ₗ[R] R[X] →ₗ[R] R[X] :=
  (LinearMap.mul R R[X]).compl₂ derivative - (LinearMap.mul R R[X]).comp derivative

@[simp]
theorem wronskianBilin_apply (a b : R[X]) : wronskianBilin R a b = wronskian a b := rfl

How can I state IsAltwronskianBilin? I tried the followings, which all didn't work (although I can prove it - whatever it is - with existing wronskian_anticomm that I may rename as wronskian_is_alt)

theorem IsAltwronskianBilin : wronskianBilin.IsAlt := by sorry
theorem IsAltwronskianBilin : LinearMap.IsAlt wronskianBilin := by sorry 

That doesn't work because Lean can't work out which R you are talking about. See my edit above for the fix, then you can write (wronskianBilin R).IsAlt.

I think I'm almost done assuming IsAltwronskianBilin (I just sorryed it and proved everything else). I have

theorem IsAltwronskianBilin : (wronskianBilin R).IsAlt := by
  intro a
  rw [wronskianBilin]
  -- sorry

and I thought ring or ring_nf would just finish from here, but it seems not.

@eric-wieser I believe it is now ready to be merged - let me know if it needs further updates.

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

maintainer merge

My one lingering question is "are you sure you don't want the n-ary wronskian instead of the binary one?". That could be written as an AlternatingMap.

If you don't want it, let's add that as a TODO in the module docstring.

I'll let someone else give this the final review, but it looks great to me now.

At least for me, I don't need it right now (for polynomial FLT). But I have an (unordinary) application in my mind that uses n-ary Wronskian. The polynomial FLT can be extended to arbitrary number of polynomials as follows: for any algebraically closed characteristic zero field $k$, the Fermat-Catalan equation

$$ a_{1}^{m_{1}} + a_{2}^{m_{2}} + \cdots + a_{n-1}^{m_{n-1}} = a_{n}^{m_{n}} $$

does not admit a non-constant solution in $k[t]$ whenever $n(n-2) \leq m_{i}$ for all $1\leq i \leq n$ (see this paper). The proof is almost same as the original Mason-Stothers theorem, and it certainly uses n-ary Wronskian. I haven't tried to formalize this proof yet, but if someone wants to formalize this (or possibly more general version that is much close to the Mason-Stothers theorem, not only for the Fermat-Catalan equations), they may need the n-ary version.

But Wronskian itself is more useful for testing linear independence of sufficiently nice functions, not only polynomials. In that direction, ultimately it would be better to define Wronskian for more general class of functions - or even for abstract rings with derivations - not only for polynomials. So I think it is fine to leave it as-is at this point.

Can you please make the linter happy? Thanks!

/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.Algebra.Polynomial.Degree.Definitions
Error: ././././Mathlib/Algebra/Polynomial/Degree/Definitions.lean:1[23](https://github.com/leanprover-community/mathlib4/actions/runs/9868167114/job/27249725253?pr=14243#step:22:24):1: error: @Polynomial.degree_ne_bot simp can prove this:
  by simp only [@ne_eq, @Polynomial.degree_eq_bot]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].

If I understood correctly, this says that the newly added theorem degree_ne_bot is somewhat duplicates with degree_eq_bot. Should I remove this from the Definitions.lean and prove the original statement in Wronskian via Polynomial.degree_eq_bot.ne?

It's just telling you to remove @[simp]

Thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style