Stream: maths

Topic: presenting a polynomial

Truong Nguyen (Apr 22 2019 at 14:40):

Hi Everyone,
I am thinking about the way that present a polynomial in Lean.
My idea is using list, for example: 1 + x + 3 x^2 will be the list: [1,1,3]. Is there a standard way of presenting it to avoid conflict.

My second question is if I want to have a Field K, how can I define it in Lean?

Mario Carneiro (Apr 22 2019 at 16:39):

field is in core, it's been there since the beginning

Mario Carneiro (Apr 22 2019 at 16:47):

polynomials are in mathlib; they are represented as finitely supported functions (eventually zero) so that leading zeros don't count as different polynomials

Truong Nguyen (Apr 22 2019 at 18:18):

Thanks you,
How to declare the field and polynomial it in VS code?
Also, where can I look for similar things, for example, if I want to declare a ring, where I can find to do it? Is there any reference in PDF file?

Chris Hughes (Apr 22 2019 at 18:33):

To prove a theorem about rings just do
lemma my_lemma {α : Type*} [ring α] : whatever

Chris Hughes (Apr 22 2019 at 18:35):

To prove your type is a ring, do something like.

def my_type : Type := sorry

instance : ring my_type :=
mul := ...
}


Truong Nguyen (Apr 23 2019 at 22:07):

Hi all,
is there any reference to see what is done or not in mathlib and in core?

Alexander Bentkamp (Apr 23 2019 at 22:32):

It's not very up to date, but there is this document: https://github.com/leanprover-community/mathlib/blob/master/docs/mathlib-overview.md

Alexander Bentkamp (Apr 23 2019 at 22:33):

I usually search the source code of mathlib, then I search the Zulip chat, and then I ask here :)

Thanks

Kevin Buzzard (Apr 24 2019 at 04:42):

I just ask here directly grin

Kevin Buzzard (Apr 24 2019 at 04:43):

Or at least, when I didn't know my way around _at all_, I just asked here. Now at least I sometimes know where to look.

Last updated: May 14 2021 at 20:13 UTC