presenting a polynomial

Stream: maths

[Truong Nguyen]

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?

[Adrian Chu]

field is already in mathlib?

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Chris Hughes]

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

def my_type : Type := sorry

instance : ring my_type :=
{  add := _,
  add_comm := _,
  mul := ...
  }

[Truong Nguyen]

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

[Alexander Bentkamp]

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]

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

[Truong Nguyen]

Thanks

[Kevin Buzzard]

I just ask here directly grin

[Kevin Buzzard]

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.