Zulip Chat Archive

Stream: general

Topic: month in mathlib (dec 2021)

Johan Commelin (Jan 03 2022 at 11:53):

There's a PR for the next "This month in mathlib" blogpost: https://github.com/leanprover-community/blog/pull/27
If you are missing an item, please add it. If you have one or two sentences that you can add about one or more PRs, please leave a suggestion.

Riccardo Brasca (Jan 03 2022 at 12:03):

We can maybe add #10350, the definition of the discriminant of a number field.

Johan Commelin (Jan 03 2022 at 12:04):

Yes, that makes sense :smile:

Patrick Massot (Jan 03 2022 at 12:05):

Riccardo, do you have one or two sentences that we could use to describe that?

Johan Commelin (Jan 03 2022 at 12:06):

Something like

- [PR #10350](https://github.com/leanprover-community/mathlib/pull/10350) introduces the discriminant of a number field (and more generally a family of vectors).

Johan Commelin (Jan 03 2022 at 12:07):

@Riccardo Brasca Was the specialization to number fields actually made in that PR?

Johan Commelin (Jan 03 2022 at 12:07):

Or is it only the general stuff?

Riccardo Brasca (Jan 03 2022 at 12:09):

Mmh, you are right, it's the general definition of the discriminant of a family of vectors.

Johan Commelin (Jan 03 2022 at 12:15):

For advertisement purposes, it would be nice to actually have the dicsr of a number field.

Arthur Paulino (Jan 03 2022 at 13:40):

@Bhavik Mehta and @Kyle Miller I wasn't able to ping you on that repo. What do you think of this description for the SRG PR?

Last updated: Dec 20 2023 at 11:08 UTC