Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Porting Wronskian.lean #46

Closed
1 task done
jcpaik opened this issue Jun 27, 2024 · 3 comments
Closed
1 task done

Porting Wronskian.lean #46

jcpaik opened this issue Jun 27, 2024 · 3 comments

Comments

@jcpaik
Copy link
Collaborator

jcpaik commented Jun 27, 2024 •
edited
Loading

  • Find the most general scalar ring/field k

My impression is that a PID scalar ring could be enough.
@jcpaik jcpaik mentioned this issue Jun 27, 2024
Closed
5 tasks
@seewoo5
Copy link
Owner

seewoo5 commented Jun 28, 2024

Wronskian can be defined for "any" ring (maybe commutative, ...) with derivation $D: R \to R$ (see RingTheory/Derivation/Basic.lean), but for now, let's generalize it to polynomial ring but with more general coefficient ring (e.g. CommRing or even SemiRing)

@seewoo5
Copy link
Owner

seewoo5 commented Jun 28, 2024

leanprover-community/mathlib4#14243

@seewoo5
Copy link
Owner

seewoo5 commented Jul 8, 2024

Related mathlib4 PRs:

@seewoo5 seewoo5 closed this as completed Jul 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@jcpaik @seewoo5