## Stream: general

#### Patrick Massot (May 12 2020 at 19:41):

One the website we have a mathlib overview. Among the problems of this list are:

• It is outdated and needs constant maintaince (spoiler: I won't propose a magic fix, we only need to care more about this list)
• It doesn't tell where are all those things, and we all know that navigating mathlib is difficult
• It doesn't point out missing things, and we have many people who want to start contributing, preferably easy things

Of course the list of missing things is open-ended. But we have a well-known half-specified milestone: covering all of undergraduate mathematics. So we could list missing undergraduate stuff, either in the main list (printed in red) or in a separate list.

#### Patrick Massot (May 12 2020 at 19:41):

In France we have a standard formatted list of undergraduate topics: the topics that are required for the agrégation, the French national exam for would be high school teachers. It changes slightly from year to year, but here is the 2020 version. It would be a very convenient first approximation, and we could modify it of course. I translated the first section (groups) and formatted it into the yaml file below. Turning that file into a webpage that looks like the mathlib overview but with links and separating missing stuff is a trivial programming exercise. My questions are: should I keep translating this list? Will there be people helping me by filling in links that I missed and editing the YaML file?

#### Patrick Massot (May 12 2020 at 19:42):

group:
basic definitions:
group: 'https://github.com/leanprover-community/lean/blob/master/library/init/algebra/group.lean#L35'
group morphism: 'https://leanprover-community.github.io/mathlib_docs/algebra/group/hom.html'
direct product of groups: 'https://leanprover-community.github.io/mathlib_docs/algebra/group/prod.html'
subgroup: 'https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html'
subgroup generated by a subset: 'https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html#group.closure'
order of an element: 'https://leanprover-community.github.io/mathlib_docs/group_theory/order_of_element.html'
normal subgroup: 'https://leanprover-community.github.io/mathlib_docs/group_theory/subgroup.html#normal_subgroup'
quotient group: 'https://leanprover-community.github.io/mathlib_docs/group_theory/quotient_group.html#quotient_group.group'
group action: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action'
stabilizer of a point: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.stabilizer'
orbit: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.orbit'
quotient space: 'https://leanprover-community.github.io/mathlib_docs/group_theory/group_action.html#mul_action.orbit_equiv_quotient_stabilizer'
class formula: ''
conjugacy classes: ''
abelian group:
cyclic group: ''
finite type abelian groups: ''
complex roots of unity: ''
primitive complex roots of unity: ''
permutation group:
permutation group of a type: 'https://leanprover-community.github.io/mathlib_docs/data/equiv/basic.html#equiv.perm'
decomposition into transpositions: ''
decomposition into cycles with disjoint support: ''
signature: 'https://leanprover-community.github.io/mathlib_docs/group_theory/perm/sign.html#equiv.perm.sign'
alternating group: ''
classical automorphim groups:
general linear group: 'https://leanprover-community.github.io/mathlib_docs/linear_algebra/basic.html#linear_map.general_linear_group'
special linear group: 'https://leanprover-community.github.io/mathlib_docs/linear_algebra/special_linear_group.html'
orthogonal group: ''
special orthogonal group: ''
unitary group: ''
special unitary group: ''
representation theory for finite groups:
representations of abelian groups: ''
Maschke theorem: ''
orthogonality of irreducible characters: ''
Fourier transform for finite abelian groups: ''
convolution: ''
examples for groups with a small cardinal: ''


#### Rob Lewis (May 12 2020 at 19:54):

I've always kind of hated the mathlib overview page (and the theories pages) because they so trivially go out of date. This looks like a step forward at least. With a fixed list of what should be there, it's easier to see when it needs to be updated.

#### Rob Lewis (May 12 2020 at 19:54):

But really, we need someone to take charge of this list and promise to keep it updated.

#### Patrick Massot (May 12 2020 at 20:04):

I think the existence of a fixed list would make it much easier. And people keep asking for projects to work on.

#### Yury G. Kudryashov (May 12 2020 at 20:29):

Some links point to the source code, some point to docs website. Is there any specific reason?

#### Patrick Massot (May 12 2020 at 21:09):

If I didn't mess up, only the core lib stuff points to code, because it has no doc.

#### Yury G. Kudryashov (May 12 2020 at 21:12):

https://leanprover-community.github.io/mathlib_docs/core/init/algebra/group.html

#### Patrick Massot (May 12 2020 at 21:22):

So you can start fixing my list. I'm sure I've also missed stuff that we already have.

#### Patrick Massot (May 12 2020 at 21:25):

I pushed my file to https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml. It isn't used for anything yet, but everybody can already fix things there.

#### Patrick Massot (May 12 2020 at 21:26):

Let's make it a test. We have one obvious suboptimal link, and a least a couple of holes that are either already here or trivial to fill. Let's see if we can get contributions there. If yes then I'll translate all the other sections.

#### Patrick Massot (May 12 2020 at 21:29):

I should also point out that one advantage of this list with precise pointers to the doc (preferably specific items rather that whole pages when it makes sense) is that we can have CI hunting for broken links at every commit. So that page would become outdated only because of additions to mathlib, not because of refactors.

#### Johan Commelin (May 13 2020 at 06:08):

@Patrick Massot I think this is a very good idea. I'll try my best to contribute, and keep contributing.

#### Yury G. Kudryashov (May 13 2020 at 06:09):

Should I push or PR?

#### Yury G. Kudryashov (May 13 2020 at 06:15):

I'd strip the common prefix from all URLs.

#### Bryan Gin-ge Chen (May 13 2020 at 06:15):

I'd say push unless there's something you want to discuss or have reviewed.

#### Johan Commelin (May 13 2020 at 06:22):

I think the broken link detector is a must btw.

#### Yury G. Kudryashov (May 13 2020 at 22:23):

I fixed some URLs and translated 1.1.

#### Bryan Gin-ge Chen (May 13 2020 at 23:00):

Should we have space for some notes in the YAML in addition to just URLs, in case mathlib's treatment of those topics deserves additional explanation?

#### Johan Commelin (May 14 2020 at 03:56):

Sounds good. And isn't YAML flexible enough to just drop those notes in?
So you write

  'cyclic_group' : blablaURL
-- or
'cyclic_group':
- URL: blablaURL
- note: '''some note'''


and the script can just figure out which of the two was used?
(Me doesn't know yaml too well.)

#### Yury G. Kudryashov (May 14 2020 at 03:59):

BTW, why do we need YAML, and not markdown with predictable structure?

#### Bryan Gin-ge Chen (May 14 2020 at 04:02):

I guess Patrick is thinking of parsing the YAML in Python and building pages from some templates somehow.

#### Yury G. Kudryashov (May 14 2020 at 04:03):

OK, let's have a YaML file

#### Yury G. Kudryashov (May 14 2020 at 04:04):

BTW, do we have an undergraduate student speaking French?

#### Yury G. Kudryashov (May 14 2020 at 04:06):

If yes, I wonder if this student will volunteer to translate the whole document. It's not too much work but I think that Patrick is overqualified for this job.

#### Yury G. Kudryashov (May 14 2020 at 04:07):

(i.e., he could use this time for something else that an undergraduate can't do)

#### Yury G. Kudryashov (May 14 2020 at 04:07):

Or I can translate in a comment, and let a student turn it into a list with links.

#### Patrick Massot (May 14 2020 at 08:10):

Yury G. Kudryashov said:

If yes, I wonder if this student will volunteer to translate the whole document. It's not too much work but I think that Patrick is overqualified for this job.

To be honest I feel I'm overqualified to write format_lean, leancrawler and leanproject, and rewriting the whole website infrastructure. One difference here is an undergrad may actually learn stuff about math and mathlib, so maybe I should dare suggest that @Ryan Lahfa would be perfect for this job.

#### Patrick Massot (May 14 2020 at 08:12):

Bryan Gin-ge Chen said:

Should we have space for some notes in the YAML in addition to just URLs, in case mathlib's treatment of those topics deserves additional explanation?

How would you like them to be displayed in the end? Actually I don't like this idea. I think this information should be in either in the module docstrings or in the theories folder if it needs to be really long.

#### Ryan Lahfa (May 14 2020 at 13:30):

Patrick Massot said:

Yury G. Kudryashov said:

If yes, I wonder if this student will volunteer to translate the whole document. It's not too much work but I think that Patrick is overqualified for this job.

To be honest I feel I'm overqualified to write format_lean, leancrawler and leanproject, and rewriting the whole website infrastructure. One difference here is an undergrad may actually learn stuff about math and mathlib, so maybe I should dare suggest that Ryan Lahfa would be perfect for this job.

I definitely can

#### Ryan Lahfa (May 14 2020 at 13:32):

Though, I don't really enjoy writing YAML and prefer TOML nowadays but that is a taste matter (and endless nights fighting with Ansible…)

#### ROCKY KAMEN-RUBIO (May 14 2020 at 13:37):

I'm happy to help with French->English translation. You just want 2020 version of the national exam topics linked in the original post right?

#### Patrick Massot (May 14 2020 at 13:57):

I don't care at all about YaML vs toml, especially if I'm not the one doing the translation. But I have a hard time thinking how the format could be simpler than what I wrote in https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

#### Patrick Massot (May 14 2020 at 13:59):

It's great that both of you want to help here. Please coordinate to avoid duplicating efforts. You can either translate without caring about what's in mathlib or do both at the same time (but please don't cheat like Johan was tempted to.

#### Ryan Lahfa (May 14 2020 at 14:04):

Patrick Massot said:

I don't care at all about YaML vs toml, especially if I'm not the one doing the translation. But I have a hard time thinking how the format could be simpler than what I wrote in https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

Indeed

#### Ryan Lahfa (May 14 2020 at 14:07):

Do we agree that real analysis should be in that overview list?

#### Ryan Lahfa (May 14 2020 at 14:08):

Like "Heine theorem", "continuity", etc.

#### Johan Commelin (May 14 2020 at 14:22):

I think the plan is to put everything from http://media.devenirenseignant.gouv.fr/file/agreg_externe/59/7/p2020_agreg_ext_maths_1107597.pdf into the YAML file. And then present it as a challenge to mathlib users to make sure that every item has a corresponding entry in mathlib.

#### Johan Commelin (May 14 2020 at 14:23):

To prevent the cheating, it might be easier to do a "dumb" translation first, without adding links to mathlib.

#### Patrick Massot (May 14 2020 at 14:27):

Ryan Lahfa said:

Like "Heine theorem", "continuity", etc.

This is all on pages 4 and 5.

#### Ryan Lahfa (May 14 2020 at 14:40):

Patrick Massot said:

Ryan Lahfa said:

Like "Heine theorem", "continuity", etc.

This is all on pages 4 and 5.

Okay, perfect ; it's clear now in my head

#### Ryan Lahfa (May 14 2020 at 14:43):

@ROCKY KAMEN-RUBIO What we can do is, I can let you backfill the current English version for links (if there's any), while I rewrite the overview_fr.yaml with french text and copy the current links over, and then, I add as much stuff as I can from the France teaching program, then you can translate it to the English version and get the links I found
We can do some iterations of this algorithm which is somewhat guaranteed to finish in few PRs

#### Ryan Lahfa (May 14 2020 at 15:04):

Quick question, @Patrick Massot @Yury G. Kudryashov wouldn't we want something like real internationalisation in the future? With something like https://weblate.org/ (they provide free instances for open source) and it's able to do automatic commits for i18n, with various review mechanisms

#### Patrick Massot (May 14 2020 at 15:05):

What would you want to translate? Here the goal is not to have both a French and and English version

#### Johan Commelin (May 14 2020 at 15:05):

I personally wouldn't worry about it too much.

#### Patrick Massot (May 14 2020 at 15:06):

It's simply that the convenient data set I was able to find happens to be in French

#### Ryan Lahfa (May 14 2020 at 15:06):

Patrick Massot said:

What would you want to translate? Here the goal is not to have both a French and and English version

Ah — Okay, it's a French → English translation only, I thought there was a goal to have a overview_fr.yaml, my apologies

#### Johan Commelin (May 14 2020 at 15:06):

We just want a long list that is a "certified and stamped" list of things that appear in an undergrad curriculum. And then pointers to mathlib.

#### Ryan Lahfa (May 14 2020 at 15:06):

Sorry for the confusion, okay, I'm writing it now then

#### Patrick Massot (May 14 2020 at 15:12):

I can see Ryan totally entered translator mode. He'll have a lot of fun once https://github.com/mpedramfar/Lean-game-maker/pull/12 will be merged. He'll be able to continue the work stated in https://github.com/ImperialCollegeLondon/natural_number_game/pull/83

#### ROCKY KAMEN-RUBIO (May 14 2020 at 17:38):

Ryan Lahfa said:

ROCKY KAMEN-RUBIO We can split the work in:
— I give you page 5 and later
— I take page < 5

Sounds good! Should we setup a shared doc to have consistent formatting?

#### Patrick Massot (May 19 2020 at 08:37):

@ROCKY KAMEN-RUBIO and @Ryan Lahfa, are you making any progress here?

#### ROCKY KAMEN-RUBIO (May 19 2020 at 15:45):

I have a draft I'll post shortly. Just tidying up some formatting

#### Ryan Lahfa (May 19 2020 at 16:23):

Patrick Massot said:

ROCKY KAMEN-RUBIO and Ryan Lahfa, are you making any progress here?

I have written some, I planned to get a working part of this today/tonight ; do you prefer small PR/improvements or rather a large PR implementing everything for this kind of changes?

#### Jalex Stark (May 19 2020 at 16:44):

the sooner you post any work, the less duplication of effort there will be, and the faster other people can make small contributions

#### Johan Commelin (May 19 2020 at 16:52):

Yup, nothing wrong with 37 small PRs!

#### ROCKY KAMEN-RUBIO (May 19 2020 at 18:34):

Here's my (still somewhat rough) draft
Aggregation_2020.pdf

#### ROCKY KAMEN-RUBIO (May 19 2020 at 18:35):

I'm still working on some of the grittier formatting. Let me know if anything is conceptually incorrect, or if you have any other suggestions.

#### Jalex Stark (May 19 2020 at 18:37):

? working hard on formatting a pdf seems wrong, since the final goal will be markdown that lives somewhere in the mathlib docs or the leanprover community website
(more to the point : post source code!)

#### Bryan Gin-ge Chen (May 19 2020 at 18:46):

Even better: I suggest opening a PR at the website repo which makes additions / edits to https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

#### Bryan Gin-ge Chen (May 19 2020 at 18:48):

Patrick Massot said:

In France we have a standard formatted list of undergraduate topics: the topics that are required for the agrégation, the French national exam for would be high school teachers. It changes slightly from year to year, but here is the 2020 version. It would be a very convenient first approximation, and we could modify it of course. I translated the first section (groups) and formatted it into the yaml file below. Turning that file into a webpage that looks like the mathlib overview but with links and separating missing stuff is a trivial programming exercise. My questions are: should I keep translating this list? Will there be people helping me by filling in links that I missed and editing the YaML file?

See this part of the first message in this thread.

#### ROCKY KAMEN-RUBIO (May 19 2020 at 18:48):

Jalex Stark said:

? working hard on formatting a pdf seems wrong, since the final goal will be markdown that lives somewhere in the mathlib docs or the leanprover community website
(more to the point : post source code!)

I guess by "grittier formatting" I meant things on the level of "clarifying that this is an exponent". I'll post my source code

#### ROCKY KAMEN-RUBIO (May 19 2020 at 18:49):

Aggregation_2020.tex

#### ROCKY KAMEN-RUBIO (May 19 2020 at 18:51):

Bryan Gin-ge Chen said:

Patrick Massot said:

In France we have a standard formatted list of undergraduate topics: the topics that are required for the agrégation, the French national exam for would be high school teachers. It changes slightly from year to year, but here is the 2020 version. It would be a very convenient first approximation, and we could modify it of course. I translated the first section (groups) and formatted it into the yaml file below. Turning that file into a webpage that looks like the mathlib overview but with links and separating missing stuff is a trivial programming exercise. My questions are: should I keep translating this list? Will there be people helping me by filling in links that I missed and editing the YaML file?

See this part of the first message in this thread.

Oh I see, don't know how I missed that. I can start putting this into the .yaml file too.

#### ROCKY KAMEN-RUBIO (May 20 2020 at 04:44):

Ok I added the definitions from sections 5 and on as a PR. I think there are redundancies, and some definitions that could be organized better, but it's a start.
https://github.com/leanprover-community/leanprover-community.github.io/compare/newsite...iceplant:patch-1

#### Bryan Gin-ge Chen (May 20 2020 at 04:52):

Great! Do you mind opening a PR? It will be easier for us to make comments and suggestions on it that way.

#### ROCKY KAMEN-RUBIO (May 23 2020 at 03:30):

Bryan Gin-ge Chen said:

Great! Do you mind opening a PR? It will be easier for us to make comments and suggestions on it that way.

I thought I opened a PR but apparently I am still a git noob and only branched. I just opened a PR for real.

#### Bryan Gin-ge Chen (May 23 2020 at 03:44):

Thank you! Here's the PR link for those who don't happen to be watching the repo: https://github.com/leanprover-community/leanprover-community.github.io/pull/26

#### ROCKY KAMEN-RUBIO (May 23 2020 at 18:01):

I'm trying to expand links to the real analysis section since I just finished @Patrick's tutorial, but I'm noticing many of the definitions are in an auxiliary file he wrote (like the definition of a convergent sequence) and I'm having trouble finding them in mathlib. Is that because they just don't exist there yet, or am I not looking in the right place?

#### Jalex Stark (May 23 2020 at 18:04):

if I go to the mathlib docs site and search for "cauchy sequence", i get useful results
https://leanprover-community.github.io/mathlib_docs/

#### Jalex Stark (May 23 2020 at 18:06):

probably the biggest barrier for you personally contributing here is in "know the words a mathematician might say"

#### Patrick Massot (May 23 2020 at 18:47):

Rocky, everything which features in the tutorial is in mathlib except for stuff used in the very last file that I haven't found time to PR. However what is in mathlib can be very hard to recognize if you know only about the elementary theory. But other people can fill this. Are you done with the translation?

#### Patrick Massot (May 23 2020 at 18:48):

And there is no point in trying to put links to mathlib before you resolve all the issues at https://github.com/leanprover-community/leanprover-community.github.io/pull/26

#### Yury G. Kudryashov (May 23 2020 at 18:53):

Many definitions and theorems about limits in mathlib are formulated in a very general form (e.g. using filters, uniformity structure, or metric_spaces).

#### ROCKY KAMEN-RUBIO (May 23 2020 at 19:16):

Yury G. Kudryashov said:

Many definitions and theorems about limits in mathlib are formulated in a very general form (e.g. using filters, uniformity structure, or metric_spaces).

That that explains a lot. I'll leave that section to others who understand this better then. Any suggestions on how to better understand these ideas? I'm familiar with filters in Haskell but haven't used them in Lean.

Patrick Massot said:

Rocky, everything which features in the tutorial is in mathlib except for stuff used in the very last file that I haven't found time to PR. However what is in mathlib can be very hard to recognize if you know only about the elementary theory. But other people can fill this. Are you done with the translation?

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

#### Patrick Stevens (May 23 2020 at 19:42):

Filters are defined in order.filter.basic - they're not the same thing as List.filter : (a -> bool) -> List a -> List a. A filter on a set U is a way of defining what it means for a subset of U to be "large and not small" in whatever sense you need "large" to mean, satisfying by definition certain "large" properties. Namely: U is itself large; a superset of a large set is large; and if you intersect two large sets then you still have a large set (that is what I meant by "not small"). It turns out to be possible to define analysis using filters on the naturals; this is closely linked to Robinson's rather lovely formulation of nonstandard analysis, but it's all very much not how you're initially taught to think about analysis, so don't expect the path to understanding to be quick. I had a quick skim of https://arxiv.org/pdf/1212.5740.pdf and it seemed reasonable

#### Bryan Gin-ge Chen (May 23 2020 at 19:44):

@Kevin Buzzard has a blogpost on filters here.

#### Patrick Massot (May 23 2020 at 19:53):

@Patrick Stevens The use of filters in mathlib has nothing to do with non-standard analysis. I think it is very unfortunate that filters can be used in non-standard analysis, since this gives a bad reputation to filters, whereas filters were nice and useful long before this application.

#### Jalex Stark (May 23 2020 at 20:01):

Some of my friends said that looking at a proof of tychonoff's theorem with filters and one without filters was the key to getting them onto the filter train

#### Jalex Stark (May 23 2020 at 20:02):

ROCKY KAMEN-RUBIO said:

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

I think patrick already suggested "resolve the issues raised at your PR" as a course of action

#### ROCKY KAMEN-RUBIO (May 23 2020 at 20:12):

Jalex Stark said:

ROCKY KAMEN-RUBIO said:

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

I think patrick already suggested "resolve the issues raised at your PR" as a course of action

I believe I resolved all the issues that were raised (to the best of my abilities, Ryan brought up some nuance in terminology that I'm not super familiar with). Is that not showing up?

#### Ryan Lahfa (May 23 2020 at 20:18):

ROCKY KAMEN-RUBIO said:

Jalex Stark said:

ROCKY KAMEN-RUBIO said:

I finished the translation, did a rudimentary formatting sweep, and submitted a PR. Let me know if there's anything else I can do!

I think patrick already suggested "resolve the issues raised at your PR" as a course of action

I believe I resolved all the issues that were raised (to the best of my abilities, Ryan brought up some nuance in terminology that I'm not super familiar with). Is that not showing up?

Let me check

#### Ryan Lahfa (May 23 2020 at 20:19):

AFAIK, our comments are still there

#### Ryan Lahfa (May 23 2020 at 20:19):

Some of them are nuance in terminology, but others are just little typos (Euler for instance)

#### Patrick Massot (May 23 2020 at 20:24):

Rocky, if you don't see the "Outdated" label in yellow as in
image.png
then you probably didn't fix an issue. Once an issue is fixed, there are two options: if you are sure you fixed it, then click the "Resolve conversation" button. Otherwise post a comment saying you tried to fix it but you're not sure

#### Patrick Massot (May 23 2020 at 20:24):

The picture shows both the oudated label and the "Resolve conversation" button

#### ROCKY KAMEN-RUBIO (May 23 2020 at 21:24):

I closed most of the issues. @Ryan Lahfa I responded to your two comments that I didn't resolve.

#### Ryan Lahfa (May 23 2020 at 21:33):

@ROCKY KAMEN-RUBIO Answered to the 2nd comment, the 1st one can be fixed in the next PR

#### Ryan Lahfa (May 23 2020 at 21:33):

@Bryan Gin-ge Chen Let us know if you like the new PR, so that I can start adding stuff on the top of it

#### Bryan Gin-ge Chen (May 23 2020 at 21:45):

@ROCKY KAMEN-RUBIO Thanks for all the fixes! @Ryan Lahfa I'll merge it now to let you work on it.

Appreciate it!

#### Ryan Lahfa (May 23 2020 at 21:53):

So the first thing is this:
https://github.com/leanprover-community/leanprover-community.github.io/pull/27
I'll do a parallel PR for backfilling links wherever I can

#### Ryan Lahfa (May 23 2020 at 21:54):

Then, maybe we can get feedback from the people in this feed at the same time on capitalization/unicode/should include LaTeX or not/etc of some points.

#### Ryan Lahfa (May 23 2020 at 23:37):

https://github.com/leanprover-community/leanprover-community.github.io/pull/28

#### Ryan Lahfa (May 29 2020 at 23:14):

https://github.com/leanprover-community/leanprover-community.github.io/pull/33 here's a PR to generate the overview page
@Bryan Gin-ge Chen @Johan Commelin I might be looking for your feedback if you will :pray:

#### Ryan Lahfa (May 29 2020 at 23:39):

I rebased https://github.com/leanprover-community/leanprover-community.github.io/pull/28 and we can merge it if we want, I think getting as much links as possible even in small increments/PRs seems a good strategy

#### Bryan Gin-ge Chen (May 30 2020 at 00:27):

At a first glance the overview page PR looks pretty good. It looks like there's still some discussion occurring around the links. I don't want to merge before getting @Patrick Massot's opinion though.

#### Johan Commelin (May 30 2020 at 05:42):

Looks good to me! Thanks for all the effort!

#### Patrick Massot (May 30 2020 at 10:08):

Thanks a lot @Ryan Lahfa . This is not yet what I had in mind, but we are getting closer. I just let a review.

#### Patrick Massot (May 30 2020 at 10:11):

PS: Ryan, using / in a git branch name is a really bad idea. It interfere with remote/branch syntax

#### Patrick Massot (May 30 2020 at 10:14):

I merged this PR anyway because we really need people to be able to contribute to the yaml file, and the layout PR also had yaml syntactic fixes (mixing both in the same PR was also not the greatest idea).

#### Patrick Massot (May 30 2020 at 10:16):

But now I cannot merge https://github.com/leanprover-community/leanprover-community.github.io/pull/28 because of conflicts. @Ryan Lahfa could you fix that really soon? I don't want to steal your commit authorship by fixing things on my side.

#### Patrick Massot (May 30 2020 at 10:19):

I don't remember whether I wrote this publicly. But I would really really like this list to be ready to be seen on Wednesday. The reason is that I've been asked to give a propaganda talk at IAS on Wednesday.

#### Patrick Massot (May 30 2020 at 10:21):

So it would be really nice for the community if we could have a overview.yaml spring filling as many links as possible. You don't even need to know any git. You can simply hit the edit button (small pen in the top right corner) to propose new links.

#### Ryan Lahfa (May 30 2020 at 10:42):

Patrick Massot said:

But now I cannot merge https://github.com/leanprover-community/leanprover-community.github.io/pull/28 because of conflicts. Ryan Lahfa could you fix that really soon? I don't want to steal your commit authorship by fixing things on my side.

Yes, I'll do it

#### Ryan Lahfa (May 30 2020 at 10:43):

Patrick Massot said:

PS: Ryan, using / in a git branch name is a really bad idea. It interfere with remote/branch syntax

AFAIK, it should not, I have been using it for ≥ 5 years, it just works fine to do remote/xxx/yyy, have you a precise example in mind?

#### Patrick Massot (May 30 2020 at 10:44):

It prevents you to skip the remote part when you want to use the default remote

#### Ryan Lahfa (May 30 2020 at 10:47):

Do you mean like git merge xxx/yyy? It'll indeed use local branches rather than origin (or whatever is the default) branches, but I can change it and replace / by -

#### Ryan Lahfa (May 30 2020 at 10:47):

I answered to some of the comments on the overview generation PR

#### Ryan Lahfa (May 30 2020 at 10:48):

As I see it, the overview backfilling links PR is fine, and should not require any further rebasing over newsite (?), so it can be merged

#### Patrick Stevens (May 30 2020 at 10:48):

It's also annoying in general for anyone who wants to do programmatic manipulation of git branches - there's nothing to prevent you naming a branch refs/heads/branchname if you want, but it similarly forces the tool-writer to get their manipulations exactly right. If the user had just not put any slashes in, the problem would be so simple, you could just split on the / character no matter what style of ref you were given

#### Patrick Stevens (May 30 2020 at 10:49):

(I have strong opinions on this - if / were simply a disallowed character in branch names, the whole system would be so much less complex)

#### Ryan Lahfa (May 30 2020 at 10:49):

Patrick Stevens said:

It's also annoying in general for anyone who wants to do programmatic manipulation of git branches - there's nothing to prevent you naming a branch refs/heads/branchname if you want, but it similarly forces the tool-writer to get their manipulations exactly right. If the user had just not put any slashes in, the problem would be so simple, you could just split on the / character no matter what style of ref you were given

But anyway, as it is possible, that sounds like sane to me for tool authors to not rely on this kind of behavior and perform exact manipulation, as they would have all the "information"

#### Ryan Lahfa (May 30 2020 at 10:49):

Patrick Stevens said:

(I have strong opinions on this - if / were simply a disallowed character in branch names, the whole system would be so much less complex)

I don't have a good visual image of how complex the system is due to this, I don't know enough git internals

#### Ryan Lahfa (May 30 2020 at 10:50):

I'll fix it in my further PRs/branches :)

#### Patrick Massot (May 30 2020 at 10:50):

Ryan Lahfa said:

As I see it, the overview backfilling links PR is fine, and should not require any further rebasing over newsite (?), so it can be merged

image.png

#### Patrick Massot (May 30 2020 at 10:50):

Ryan Lahfa said:

Do you mean like git merge xxx/yyy? It'll indeed use local branches rather than origin (or whatever is the default) branches, but I can change it and replace / by -

I mean git fetch

#### Ryan Lahfa (May 30 2020 at 10:51):

Patrick Massot said:

Ryan Lahfa said:

As I see it, the overview backfilling links PR is fine, and should not require any further rebasing over newsite (?), so it can be merged

image.png

My GitHub UI seems to be outdated/stuck, I'll rebase it again to ensure everything is fine

Done

#### Ryan Lahfa (May 30 2020 at 10:52):

Patrick Massot said:

Ryan Lahfa said:

Do you mean like git merge xxx/yyy? It'll indeed use local branches rather than origin (or whatever is the default) branches, but I can change it and replace / by -

I mean git fetch

Okay, that's a fair point :-)

#### Patrick Massot (May 30 2020 at 10:55):

Thanks for rebasing. I merged it. So now everybody can contribute to filling more links.

#### Ryan Lahfa (May 30 2020 at 10:55):

Also, @Patrick Massot @Bryan Gin-ge Chen wonder if I could get commit access to the repository (w/o master or newsite for example), that'd make a simpler workflow for some PRs which might be edited on the top (e.g. links backfilling)

#### Patrick Massot (May 30 2020 at 10:56):

Could you try to use some TeX in this yaml file? Mathjax is loaded on all pages of the website. So if the yaml parser doesn't get confused then it should work. And if it does get confused then maybe enclosing stuff in quote would be good enough to unconfuse it.

#### Ryan Lahfa (May 30 2020 at 10:57):

@Patrick Massot I was definitely going to try this

#### Ryan Lahfa (May 30 2020 at 10:57):

I can replace the Unicode math by some LaTeX

#### Ryan Lahfa (May 30 2020 at 10:57):

The result might be ugly though, like if you do inline math in respect to the line height (?), but I'm no expert, we'll see and I'll post about it

#### Patrick Massot (May 30 2020 at 10:58):

I see that real numbers don't even have a unicode mathbb.

:-)

#### Ryan Lahfa (May 30 2020 at 10:59):

That's an easy fix s/R/$\mathbb{R}$/g

#### Patrick Massot (May 30 2020 at 10:59):

About the repo access, I'd be happy to give you write access to branches that are not master or newsite, but I'm not sure this wouldn't mess up CI (if I need to protect branches or something), so I'll let Bryan handle that.

#### Ryan Lahfa (May 30 2020 at 11:00):

Patrick Massot said:

About the repo access, I'd be happy to give you write access to branches that are not master or newsite, but I'm not sure this wouldn't mess up CI (if I need to protect branches or something), so I'll let Bryan handle that.

Sure thing

#### Ryan Lahfa (May 30 2020 at 11:01):

@Patrick Massot Also, should we just use complex.xxx for the link syntax

#### Ryan Lahfa (May 30 2020 at 11:01):

And use mathlib_docs/find/{{ decl }}

#### Ryan Lahfa (May 30 2020 at 11:01):

Sounds like an easy way to fill links, e.g. https://leanprover-community.github.io/mathlib_docs/find/complex.exists_root for complex.exists_root

#### Ryan Lahfa (May 30 2020 at 11:02):

(I mean rather the module.statement syntax rather than the folder1/folder2/module.html#statement or whatever)

#### Patrick Massot (May 30 2020 at 11:06):

The advantage of the current format is you can fill in items while browsing the doc website and copy-pasting partial links

#### Patrick Massot (May 30 2020 at 11:07):

And also a dot separated format looks like Lean namespacing and we don't have any convenient way to access the fully qualified name of a declaration while staring at the file containing it.

#### Ryan Lahfa (May 30 2020 at 11:14):

isn't it just whatever the statement of a declaration we're looking at?

@Rob Lewis ^

#### Ryan Lahfa (May 30 2020 at 11:14):

But alright, I was just finding the process of browsing/copying a bit slow for massive link injection

#### Ryan Lahfa (May 30 2020 at 11:15):

But that's the computer scientist in me who is talking, pay no heed

#### Scott Morrison (May 30 2020 at 11:17):

The problem when looking at a declaration is that it can be hard to work out what namespace you're currently in (because so many mathlib files are so long). You can insert a #where to discover the namespace, but this will cause recompilation headaches if you're jumping between many files.

#### Ryan Lahfa (May 30 2020 at 11:18):

Okay, that's not very usable for browsing docs → injecting them in the YAML file, thanks for the clarification

#### Rob Lewis (May 30 2020 at 11:20):

Yes, the /find/ page just takes a (complete) identifier. Notice that the docs always print a complete identifier, so if you look at (randomly) docs#std.prec.max_plus you can copy std.prec.max_plus directly. It's trickier to find this browsing the Lean source, but you can keep a file with import all open and just use tab complete.

#### Rob Lewis (May 30 2020 at 11:21):

It's easy enough to expose the declaration name -> location map from the doc generator if this is useful.

#### Rob Lewis (May 30 2020 at 11:23):

The benefit to using this over hardcoded links, of course, is that if a declaration is moved to a new file the links won't break. Even more important if you're linking to lines in the source, which are very likely to break. src#std.prec.max_plus will stay up to date.

#### Ryan Lahfa (May 30 2020 at 11:27):

Maybe what we can do now is to use hardcoded links, then we can do an automatic pass to rewrite them properly using the complete identifier, so we can hit the deadline of the IAS for @Patrick Massot

#### Ryan Lahfa (May 30 2020 at 11:28):

But decl name → location map would be useful I guess, I don't know if it has to be exposed in the HTML or as a JSON/YAML machine-consumable

#### Rob Lewis (May 30 2020 at 11:29):

Your links already contain the complete identifier, right? I see things like algebra/pi_instances.html#prod.module. Everything after the # is the complete identifier.

#### Rob Lewis (May 30 2020 at 11:31):

Ryan Lahfa said:

But decl name → location map would be useful I guess, I don't know if it has to be exposed in the HTML or as a JSON/YAML machine-consumable

It wouldn't change the HTML at all, would just host a file leanprover-community.github.io/mathlib_docs/name_to_loc.json.

#### Rob Lewis (May 30 2020 at 11:31):

So if the website generator needed this info it could just grab the map there.

#### Rob Lewis (May 30 2020 at 11:32):

It could include more info too, e.g. the type of the declaration. I think this would be particularly nice for the 100 theorems list, to print the statement on the main page.

#### Ryan Lahfa (May 30 2020 at 11:46):

Rob Lewis said:

Your links already contain the complete identifier, right? I see things like algebra/pi_instances.html#prod.module. Everything after the # is the complete identifier.

Well, this was something I grabbed from the doc link, so I didn't know if it was complete or not

#### Ryan Lahfa (May 30 2020 at 11:46):

Sounds good @Rob Lewis — I'll see what I can do, but maybe after IAS to make it cooler

#### Mario Carneiro (May 30 2020 at 12:07):

Scott Morrison said:

The problem when looking at a declaration is that it can be hard to work out what namespace you're currently in (because so many mathlib files are so long). You can insert a #where to discover the namespace, but this will cause recompilation headaches if you're jumping between many files.

Earlier, someone (Kevin?) suggested that we could have theorem declarations be hoverable same as theorem uses. If the hover contained the full namespaced name, wouldn't that solve the problem?

Yes

#### Johan Commelin (May 30 2020 at 13:07):

Can someone (@Patrick Massot @Ryan Lahfa ?) tell me how complete the .yaml now is?
Is it just a matter of filling in the links, or are there also still new sections that need to be added to the .yaml?

#### Patrick Massot (May 30 2020 at 13:08):

Filling the links would be awesome

#### Patrick Massot (May 30 2020 at 13:09):

We don't plan to add sections soon. At some point we'll probably want to add more advanced sections, maybe in another file.

#### Johan Commelin (May 30 2020 at 13:09):

Which years does this cover? Is this like 1st and 2nd year of French math education?

#### Johan Commelin (May 30 2020 at 13:09):

How should I interpret this file?

#### Johan Commelin (May 30 2020 at 13:11):

http://media.devenirenseignant.gouv.fr/file/agreg_externe/59/7/p2020_agreg_ext_maths_1107597.pdf
to the top of the file, in a comment?

#### Johan Commelin (May 30 2020 at 13:11):

Is this file already rendered somewhere on a public facing website?

#### Patrick Massot (May 30 2020 at 13:12):

There is a semi-hidden temporary rendering at https://leanprover-community.github.io/overview.html, but really you should ignore that and just fill in

#### Johan Commelin (May 30 2020 at 13:23):

What is the correct link for complementary subspaces: https://leanprover-community.github.io/mathlib_docs/linear_algebra/projection.html ? Do we have a statement that says that you can choose such a subspace? (@Yury G. Kudryashov)

#### Patrick Massot (May 30 2020 at 13:25):

Hmm, https://leanprover-community.github.io/mathlib_docs/order/bounded_lattice.html#is_compl might be a bit too abstract...

Exactly

#### Patrick Massot (May 30 2020 at 13:29):

It's still useful information that this is how it's said in mathlib. And we can always add more context in https://leanprover-community.github.io/theories/linear_algebra.html

#### Yury G. Kudryashov (May 30 2020 at 13:33):

Do we allow multiple links per item?

#### Yury G. Kudryashov (May 30 2020 at 13:33):

https://leanprover-community.github.io/mathlib_docs/linear_algebra/basis.html#submodule.exists_is_compl states that a complementary subspace exists.

#### Patrick Massot (May 30 2020 at 13:37):

There is no issue putting several links per item in the yaml file, but that would be hard to render if we want to keep it compact (where each listed item is a link to something).

#### Johan Commelin (May 30 2020 at 13:37):

We still don't have Cayley–Hamilton

#### Patrick Massot (May 30 2020 at 13:37):

Yes, this is one of the goal of this list: highlighting glaring holes (although this is not how I intend to use it on Wednesday...).

#### Johan Commelin (May 30 2020 at 13:39):

https://github.com/leanprover-community/leanprover-community.github.io/pull/36 is what I've found for section 1.

#### Yury G. Kudryashov (May 30 2020 at 13:40):

Should we show formalized and not yet formalized items on different pages?

#### Patrick Massot (May 30 2020 at 13:41):

Yes, I think they should be on different pages

#### Johan Commelin (May 30 2020 at 13:41):

Maybe just an option at the top

#### Johan Commelin (May 30 2020 at 13:41):

Where you can toggle what you want to see.

#### Johan Commelin (May 30 2020 at 13:41):

With a bit of CSS classes that should be trivial

#### Patrick Massot (May 30 2020 at 13:42):

True, but we also want to browse the TODO list, without seeing what is done

#### Johan Commelin (May 30 2020 at 13:46):

That's what I'm saying, right?

#### Johan Commelin (May 30 2020 at 13:46):

Two radio buttons should be able to provide that.

#### Johan Commelin (May 30 2020 at 13:46):

Done: on/off     TODO: on/off

#### Patrick Massot (May 30 2020 at 13:50):

Oh ok, right. Feel free to implement, or hope Ryan will do it.

#### Patrick Massot (May 30 2020 at 14:01):

Johan Commelin said:

https://github.com/leanprover-community/leanprover-community.github.io/pull/36 is what I've found for section 1.

Merged, thanks!

#### Ryan Lahfa (May 30 2020 at 14:08):

Johan Commelin said:

Done: on/off     TODO: on/off

Sounds good

I'm doing it now

#### Johan Commelin (May 30 2020 at 14:27):

Coprime elements: we have coprime ideals (ideal.is_coprime) but not specifically coprime elements. To do or not to do?

#### Ryan Lahfa (May 30 2020 at 14:30):

I guess it's "alright"

#### Johan Commelin (May 30 2020 at 14:40):

@Patrick Massot Does the "boss" have an opinion? :wink:

#### Yury G. Kudryashov (May 30 2020 at 14:45):

ideal.is_coprime is a definition of coprime elements that uses ideals.

#### Johan Commelin (May 30 2020 at 14:47):

Ooh, that's an ugly name in that case

#### Johan Commelin (May 30 2020 at 14:48):

Divisibility in commutative integral rings what does this mean? What's an integral ring?

#### Kevin Buzzard (May 30 2020 at 14:50):

I guess for a general ring one can make sense of coprimality of two elements by just asking $(a)+(b)=R$, but then $X$ and $Y$ would not be coprime in $\mathbb{C}[X,Y]$.

#### Johan Commelin (May 30 2020 at 14:53):

What the hack is a Rupture fields:?

splitting field?

#### Johan Commelin (May 30 2020 at 14:54):

Nope, that's the next item

#### Johan Commelin (May 30 2020 at 14:55):

https://github.com/leanprover-community/leanprover-community.github.io/pull/37 here's a bunch of links for section 3 (@Patrick Massot)

#### Chris Hughes (May 30 2020 at 14:55):

It's just the field when you adjoin one root, but not necessarily all of them

#### Johan Commelin (May 30 2020 at 14:55):

So we have that, right?

Yes

#### Alex J. Best (May 30 2020 at 14:55):

https://fr.wikipedia.org/wiki/Corps_de_rupture

#### Johan Commelin (May 30 2020 at 14:56):

Derived polynomials: # Should this be "Polynomial derivative"? @Ryan Lahfa

#### Ryan Lahfa (May 30 2020 at 14:56):

@Johan Commelin Yes, it's really $P'$ when $P$ is a polynomial IIRC

#### Ryan Lahfa (May 30 2020 at 14:56):

as a formal polynomial

#### Reid Barton (May 30 2020 at 14:56):

https://en.wikipedia.org/wiki/Rupture_field

#### Ryan Lahfa (May 30 2020 at 14:56):

I was going to link it :D

#### Reid Barton (May 30 2020 at 14:57):

I definitely assumed this was a mistranslation

#### Ryan Lahfa (May 30 2020 at 14:57):

I double checked those because it looked fishy to me but Wikipedia proved me wrong

TIL

#### Ryan Lahfa (May 30 2020 at 14:57):

But really, sometimes, in France, there seems to be many structures which are not "directly" available in English

#### Ryan Lahfa (May 30 2020 at 14:57):

Also, our convergence is not the good one :-°

#### Ryan Lahfa (May 30 2020 at 14:59):

We call a limit, something which is rather limit by different values $\lim_{x \to a \atop x \neq a} f(x)$ (for example)

#### Ryan Lahfa (May 30 2020 at 14:59):

But it does not matter

#### Johan Commelin (May 30 2020 at 14:59):

I've pushed those two fixes

#### Ryan Lahfa (May 30 2020 at 15:02):

I have the desired feature

Will push it

#### Johan Commelin (May 30 2020 at 15:04):

Ryan Lahfa said:

I have the desired feature

Yes

#### Ryan Lahfa (May 30 2020 at 15:04):

https://github.com/leanprover-community/leanprover-community.github.io/pull/38

#### Ryan Lahfa (May 30 2020 at 15:05):

Awesome PRs @Johan Commelin

#### Ryan Lahfa (May 30 2020 at 15:05):

We should try to use LaTeX for titles

#### Ryan Lahfa (May 30 2020 at 15:06):

Like "something something $\Q[X]$ something" if we have the macro for, or just $\mathbb{Q}$

#### Ryan Lahfa (May 30 2020 at 15:07):

Screen-Capture_select-area_20200530170650.png

#### Ryan Lahfa (May 30 2020 at 15:07):

LaTeX is working just fine

#### Ryan Lahfa (May 30 2020 at 15:07):

Will do a PR to add some examples

#### Ryan Lahfa (May 30 2020 at 15:07):

of course, we don't have the macro \Q

#### Ryan Lahfa (May 30 2020 at 15:07):

should we add some macros to our MathJax setup?

#### Johan Commelin (May 30 2020 at 15:07):

You could add some common macros to the top of the rendered page.

#### Ryan Lahfa (May 30 2020 at 15:08):

Alright, I'll do it

#### Ryan Lahfa (May 30 2020 at 15:08):

Shouldn't I do this in templates/_base.html ?

Je ne sais pas

#### Ryan Lahfa (May 30 2020 at 15:08):

I'll try locally, if it works fine, I'll let as-is and @Patrick Massot will do the ultimate call

:D

#### Ryan Lahfa (May 30 2020 at 15:12):

Does not work, so I'll put it in the base

#### Patrick Massot (May 30 2020 at 15:20):

I'm sorry I was away. Are there still things to discuss, or did you settle everything?

#### Ryan Lahfa (May 30 2020 at 15:20):

https://github.com/leanprover-community/leanprover-community.github.io/pull/39

#### Ryan Lahfa (May 30 2020 at 15:21):

@Patrick Massot You can take a look to 39 & 38 and see if it's okay for you

#### Patrick Massot (May 30 2020 at 15:21):

I think we can add a couple of LaTeX macros in _base.html.

#### Ryan Lahfa (May 30 2020 at 15:21):

39 implements the LaTeX macros in _base

#### Ryan Lahfa (May 30 2020 at 15:21):

I didn't go too far, I just added R, Q, Z, C, N

#### Ryan Lahfa (May 30 2020 at 15:22):

We could add GL, L, class{n} (continuity classes), S(R^d), etc. Depends.

#### Johan Commelin (May 30 2020 at 15:22):

@Patrick Massot By now, my PR should be uncontroversial.

#### Johan Commelin (May 30 2020 at 15:23):

I think GL, SL, etc are fine. But I wouldn't go overboard with the macros.

#### Ryan Lahfa (May 30 2020 at 15:23):

I do mathrm{GL}, etc. for them

#### Ryan Lahfa (May 30 2020 at 15:23):

You can see it in 39

#### Johan Commelin (May 30 2020 at 15:23):

Maybe the rule of three applies? If you need it more then 3 times, a macro should be fine.

#### Ryan Lahfa (May 30 2020 at 15:23):

GL(n, R), GL(n, C)…

#### Patrick Massot (May 30 2020 at 15:23):

Are those 3 PRs compatible?

#### Ryan Lahfa (May 30 2020 at 15:23):

O(n, 2), O(n, 3)…

#### Ryan Lahfa (May 30 2020 at 15:23):

@Patrick Massot Please merge Johan's ones first

#### Ryan Lahfa (May 30 2020 at 15:24):

Then I'll do the rebase magic for whatever happens

#### Ryan Lahfa (May 30 2020 at 15:24):

I'm pretty sure there are no to very few conflicts

#### Ryan Lahfa (May 30 2020 at 15:25):

(we're close to have everything in rings, wow!)

#### Johan Commelin (May 30 2020 at 15:25):

@Patrick Massot One second

#### Johan Commelin (May 30 2020 at 15:25):

Ryan spotted an issue in my PR

#### Ryan Lahfa (May 30 2020 at 15:25):

@Johan Commelin it's not that important, I'm fixing it in my PR

#### Ryan Lahfa (May 30 2020 at 15:26):

If you don't do it, that'll just break newsite temporarily (before merging mine)

#### Johan Commelin (May 30 2020 at 15:27):

@Patrick Massot Ok, you can merge now

#### Patrick Massot (May 30 2020 at 15:27):

I reviewed Johan's PR

#### Patrick Massot (May 30 2020 at 15:28):

But I could merge it since my comments are only about empty items

#### Ryan Lahfa (May 30 2020 at 15:28):

Yes, I think we can merge it

#### Johan Commelin (May 30 2020 at 15:28):

Also, I need to go now

#### Patrick Massot (May 30 2020 at 15:30):

Thanks Johan, I merged it.

#### Ryan Lahfa (May 30 2020 at 15:30):

Fixing the conflicts

#### Ryan Lahfa (May 30 2020 at 15:33):

Conflicts resolved, @Patrick Massot

#### Ryan Lahfa (May 30 2020 at 15:35):

I'll experiment for the "show inline elements for the last depth level"

Great!

#### Ryan Lahfa (May 30 2020 at 15:38):

@Patrick Massot style question, should we do titlecase for every title?

#### Patrick Massot (May 30 2020 at 15:38):

I merged the switch one and this created conflict in the macro one

#### Ryan Lahfa (May 30 2020 at 15:38):

I'll fix the macro one

#### Patrick Massot (May 30 2020 at 15:39):

About titlecase, let's do whatever is convenient in the yaml, and we can add a jinja filter if we want to change it on the website

#### Ryan Lahfa (May 30 2020 at 15:40):

At the make_site phase, we can just give title.titlecase() if we want, it was really just should we do it or not?

#### Patrick Massot (May 30 2020 at 15:40):

The title of the page should change too. I think we can use "Undergraduate mathematics in mathlib".

#### Ryan Lahfa (May 30 2020 at 15:41):

@Patrick Massot conflicts resolved on the latex one

#### Ryan Lahfa (May 30 2020 at 15:42):

:-)

screencapture-leanprover-community-github-io-overview-html-2020-05-30-17_42_06.png

#### Patrick Massot (May 30 2020 at 15:44):

We try to checkout your PR 40 it doesn't seem to work

#### Patrick Massot (May 30 2020 at 15:44):

Does it work on your end?

#### Ryan Lahfa (May 30 2020 at 15:44):

Patrick Massot said:

We try to checkout your PR 40 it doesn't seem to work

Maybe I misunderstood what do you mean by inline elements, is it like the latest nodes are not accordion, right?

#### Patrick Massot (May 30 2020 at 15:46):

I want the deepest level to be a single paragraph, with words separated by commas. As in the original document

#### Patrick Massot (May 30 2020 at 15:46):

On your screenshot, everything under "Bilinear" would be on the same line

#### Ryan Lahfa (May 30 2020 at 15:47):

Oh okay, makes sense, and all "mathematical statements" would be <a /> to the docs, right?

#### Patrick Massot (May 30 2020 at 15:48):

And there would be no "See it in mathlib documentation" anywhere. Instead of use card containing

vector space
See it in mathlib documentation


and a huge card linear map..., there would be

I see

I'm doing it

#### Ryan Lahfa (May 30 2020 at 15:49):

I should have the prototype in minutes

#### Patrick Massot (May 30 2020 at 15:49):

Thank you very much

#### Ryan Lahfa (May 30 2020 at 15:50):

@Patrick Massot Just a quick question

Yes?

#### Ryan Lahfa (May 30 2020 at 15:50):

xxx:
yyy: …
zzz: …
ttt:
aaa: …
uuu: …


#### Ryan Lahfa (May 30 2020 at 15:51):

do you show in the xxx card:
yyy, zzz
then the ttt accordion
then uuu?

#### Patrick Massot (May 30 2020 at 15:52):

We probably need to simplify the nesting. I think there should be only two levels of accordions.

Agreed

#### Patrick Massot (May 30 2020 at 15:52):

Do you have a specific example?

#### Ryan Lahfa (May 30 2020 at 15:52):

Take linear algebra

#### Ryan Lahfa (May 30 2020 at 15:52):

Linear algebra:
vector space: 'algebra/module.html#vector_space'
linear map: 'algebra/module.html#linear_map'
product of vector spaces: 'algebra/pi_instances.html#prod.module'
vector subspace: 'algebra/module.html#subspace'
range of a linear map: 'linear_algebra/basic.html#linear_map.range'
kernel of a linear map: 'linear_algebra/basic.html#linear_map.ker'
quotient space: 'linear_algebra/basic.html#submodule.quotient'
sum of subspaces: 'linear_algebra/basic.html#submodule.complete_lattice'
direct sum: ''
complement subspace: ''
linear independent: 'linear_algebra/basis.html#linear_independent'
generating sets: ''
bases: ''
algebra of endomorphisms of a vector space: ''
general linear group: 'linear_algebra/basic.html#linear_map.general_linear_group'
invariant subspace of an endomorphism: ''
eigenvalue: ''
eigenvector: ''
linear representation: ''
irreducible representation: ''
finite dimensional representations:
examples: ''
Schur's lemma: ''
finite-dimensional vector spaces:
finite-dimensional vector spaces: 'linear_algebra/finite_dimensional.html#finite_dimensional'
existence of bases: 'linear_algebra/basis.html#exists_is_basis'
canonical isomorphism with K^n: 'linear_algebra/basis.html#module_equiv_finsupp'
complementary subspaces: 'linear_algebra/basis.html#submodule.exists_is_compl'
rank of a linear map: ''
rank of a set of vectors: ''
dual vector space: 'linear_algebra/dual.html#module.dual'
rank of a system of linear equations: ''
transpose of a linear map: ''
dual basis: 'linear_algebra/dual.html#is_basis.dual_basis'
bidual: 'linear_algebra/dual.html#vector_space.eval_equiv'
orthogonality: ''
multilinear:
multilinear map: 'linear_algebra/multilinear.html#multilinear_map'
determinant of vectors: ''
determinant of endomorphisms: ''
special linear group: ''
orientation of a R-valued vector space: ''
matrices:
commutative ring valued matrices: 'data/matrix/basic.html#matrix'
field valued matrices: 'data/matrix/basic.html#matrix'
elementary operations on matrices' rows: ''
elementary operations on matrices' columns: ''
determinant: 'linear_algebra/determinant.html#matrix.det'
invertibility: 'linear_algebra/nonsingular_inverse.html#matrix.nonsing_inv'
rank of a matrix: ''
matrix representation of a linear map: 'linear_algebra/matrix.html#linear_map.to_matrix'
coordinates change: ''
Gauss' pivot: ''
row-reduced matrices: ''
endomorphism invariant subspaces: ''
kernel lemma: ''
characteristic polynomial: ''
endomorphism polynomials: ''
cancelling polynomials: ''
minimal polynomial: ''
Cayley-Hamilton theorem: ''


#### Ryan Lahfa (May 30 2020 at 15:53):

necessarily, I need a way to determine when to stop the inline display for leaves

#### Ryan Lahfa (May 30 2020 at 15:53):

I think I can work out some prototype but just want to warn about the strange result it might give

#### Patrick Massot (May 30 2020 at 15:54):

Here I think we are actually missing nesting. The issue is that some stuff is dumped at level 2 but should be level 3 (ie leaves).

#### Ryan Lahfa (May 30 2020 at 15:55):

I think too, I didn't work on the organization and wanted to get something out ASAP

#### Patrick Massot (May 30 2020 at 15:56):

The end is clearly missing a heading, something like 'endomorphism polynomials'

#### Ryan Lahfa (May 30 2020 at 15:56):

Anyway, I'll implement the following solution:
When I encounter a leaf, I just show it inline with <a /> and add a ,  if I'm not the last node of the current iterator (doable in Jinja magic)
When I encounter an internal node, I create an accordion
That should work

#### Ryan Lahfa (May 30 2020 at 15:56):

Patrick Massot said:

The end is clearly missing a heading, something like 'endomorphism polynomials'

We already have endomorphism polynomials, but you have this annoying issue
Then you have to repeat it in order to link to the concept

#### Ryan Lahfa (May 30 2020 at 15:57):

Like, endomorphism polynomials have a lot of things around, but are themselves a specific kind of polynomials… I don't know how to solve "this"

#### Patrick Massot (May 30 2020 at 15:57):

I don't think this is a big issue

Okay

#### Patrick Massot (May 30 2020 at 15:58):

You can let people with more math experience going over the yaml file to sort this out

#### Ryan Lahfa (May 30 2020 at 15:59):

screencapture-localhost-8000-overview-html-2020-05-30-17_59_00.png

#### Ryan Lahfa (May 30 2020 at 15:59):

@Patrick Massot Yes, definitely, I don't want to fight this :) — I'm still too green

#### Ryan Lahfa (May 30 2020 at 15:59):

Here's a prototype

#### Ryan Lahfa (May 30 2020 at 16:00):

Do you want I do something before I commit this?

#### Patrick Massot (May 30 2020 at 16:00):

I think it looks much better. But there is still the issue that inner card should extend horizontally to match outer ones

#### Ryan Lahfa (May 30 2020 at 16:02):

Screen-Capture_select-area_20200530180156.png
do you mean something like this ?

#### Ryan Lahfa (May 30 2020 at 16:02):

because all cards applied padding on their stuff, so when I nest them, obviously…

#### Ryan Lahfa (May 30 2020 at 16:03):

but I don't think that's a bad thing per se, that gives space and looks not that bad on mobile AFAIK

#### Ryan Lahfa (May 30 2020 at 16:04):

we can reduce padding in the inner cards I guess

#### Patrick Massot (May 30 2020 at 16:08):

No, I mean no space at all on sides of inner cards.

#### Patrick Massot (May 30 2020 at 16:09):

Also I'd prefer to keep a white background. It looks weird to have this all grey background only on this webpage of the website

#### Ryan Lahfa (May 30 2020 at 16:12):

Okay for bg color

#### Ryan Lahfa (May 30 2020 at 16:13):

For the space, I'll try something, you'll let me know, worst case, you can edit the PR or guide me again

#### Ryan Lahfa (May 30 2020 at 16:13):

Should have something in 10 minutes hopefully

#### Patrick Massot (May 30 2020 at 16:14):

Also, I'm not the only one deciding stuff here. If everybody likes those margins I'll have them.

#### Ryan Lahfa (May 30 2020 at 16:15):

Then we should ping them for their advice, @Bryan Gin-ge Chen @Rob Lewis @Kevin Buzzard @Yury G. Kudryashov @Mario Carneiro @Scott Morrison

#### Patrick Massot (May 30 2020 at 16:18):

You should have waited to get a prototype incorporating everything (including switches and updated page title)

Why?

#### Patrick Massot (May 30 2020 at 16:19):

Because this way they don't have to read all messages, they can look at the result

#### Patrick Massot (May 30 2020 at 16:19):

Those are busy people

You're right

Apologies

Don't worry

#### Ryan Lahfa (May 30 2020 at 16:24):

It's now online on the inline branch, @Patrick Massot

#### Ryan Lahfa (May 30 2020 at 16:24):

It is also rebased over newsite, I'll just verify & repull just in case

#### Kevin Buzzard (May 30 2020 at 16:24):

Did somebody call?

#### Kevin Buzzard (May 30 2020 at 16:25):

I am just having a break from marking, what should I look at?

#### Kevin Buzzard (May 30 2020 at 16:25):

Only 80 algebraic geometry questions to go :D

#### Ryan Lahfa (May 30 2020 at 16:26):

I'm getting full page screenshots, if you don't want to do make_site on the branch

#### Ryan Lahfa (May 30 2020 at 16:27):

Let us know what you think of the design and what would you want to see

#### Ryan Lahfa (May 30 2020 at 16:28):

https://github.com/leanprover-community/leanprover-community.github.io/pull/40

#### Patrick Massot (May 30 2020 at 16:28):

There is something funny going on with "Affine and Euclidian Geoemtry (finite dimensional only)" (besides the typo and the restriction)

#### Ryan Lahfa (May 30 2020 at 16:28):

The PR is there for the ones who want to try it live

#### Ryan Lahfa (May 30 2020 at 16:28):

@Patrick Massot YAML stuff most likely

#### Ryan Lahfa (May 30 2020 at 16:29):

Can fix it in a future PR

#### Patrick Massot (May 30 2020 at 16:30):

I'd like the accordion to be folded when you open the page, so that people can navigate quickly. And also the todo switch should be off by default, so that people first get the information about what is there and where.

#### Patrick Massot (May 30 2020 at 16:31):

And I still don't like the horizontal margins :stuck_out_tongue:

#### Patrick Massot (May 30 2020 at 16:31):

But otherwise it really starts looking like what I dreamed of.

#### Ryan Lahfa (May 30 2020 at 16:31):

Patrick Massot said:

I'd like the accordion to be folded when you open the page, so that people can navigate quickly. And also the todo switch should be off by default, so that people first get the information about what is there and where.

• Default switch to off is easy for TODO
• Folded accordions is easy too

Can add them, right now, should I go for it?

#### Ryan Lahfa (May 30 2020 at 16:32):

Patrick Massot said:

And I still don't like the horizontal margins :stuck_out_tongue:

I will have to wait the vote from the people

#### Mario Carneiro (May 30 2020 at 16:32):

those screenshots are massive and zulip doesn't let me zoom in easily. could you show a representative sample?

#### Patrick Massot (May 30 2020 at 16:32):

You'll have more votes when I'll merge the PR and we'll see it live

#### Ryan Lahfa (May 30 2020 at 16:32):

@Mario Carneiro You can load them in your browser or enable pan & zoom to review them easily

#### Ryan Lahfa (May 30 2020 at 16:32):

But yes, let's merge the PR @Patrick Massot

#### Patrick Massot (May 30 2020 at 16:32):

when I click on them it zooms

#### Ryan Lahfa (May 30 2020 at 16:32):

Let me just get the latest changes you want

#### Patrick Massot (May 30 2020 at 16:32):

Did you fixed the two defaults?

#### Patrick Massot (May 30 2020 at 16:32):

Yes, let's do that

#### Ryan Lahfa (May 30 2020 at 16:33):

I'm doing it, only one left

#### Mario Carneiro (May 30 2020 at 16:33):

with pan & zoom the frame doesn't change shape so I'm peering through a very slim vertical window

#### Mario Carneiro (May 30 2020 at 16:34):

zulip's implementation really needs work

#### Patrick Massot (May 30 2020 at 16:34):

Mario, you should hold on for 5 minutes

#### Ryan Lahfa (May 30 2020 at 16:34):

Just open the link in the browser

#### Mario Carneiro (May 30 2020 at 16:35):

what is being reviewed?

the margins?

#### Ryan Lahfa (May 30 2020 at 16:35):

@Mario Carneiro the looks mostly

#### Mario Carneiro (May 30 2020 at 16:35):

the spacing is all over the place

#### Mario Carneiro (May 30 2020 at 16:36):

there is 0px spacing between cards but significant (20px?) margins on left and right and at the bottom of a group

#### Ryan Lahfa (May 30 2020 at 16:36):

here we go for the defaults

#### Mario Carneiro (May 30 2020 at 16:36):

also there is no spacing after the text and before the cards

#### Ryan Lahfa (May 30 2020 at 16:37):

+1 @ spacing pre/post cards

#### Ryan Lahfa (May 30 2020 at 16:37):

the indentation "spacing" is by default

#### Mario Carneiro (May 30 2020 at 16:37):

What's wrong with a simple bullet list?

#### Ryan Lahfa (May 30 2020 at 16:37):

it's not an accordion (?)

#### Ryan Lahfa (May 30 2020 at 16:37):

you can fold/unfold those cards

#### Ryan Lahfa (May 30 2020 at 16:38):

@Patrick Massot wants to remove horizontal space on cards I think (if I understood well, I won't speak in its place)

#### Mario Carneiro (May 30 2020 at 16:38):

I'm not sure why this particular list is getting web-designed

#### Patrick Massot (May 30 2020 at 16:38):

I don't understand why it doesn't look like https://getbootstrap.com/docs/4.4/components/collapse/#accordion-example

#### Mario Carneiro (May 30 2020 at 16:38):

I would have just chucked some markdown on a page

#### Patrick Massot (May 30 2020 at 16:38):

Mario, this list is too big to be unfolded by default

#### Ryan Lahfa (May 30 2020 at 16:38):

@Patrick Massot I can take a look why

#### Ryan Lahfa (May 30 2020 at 16:38):

It might be a class missing

#### Mario Carneiro (May 30 2020 at 16:39):

I've seen mile long bullet lists before

#### Patrick Massot (May 30 2020 at 16:39):

Mario didn't need CSS in metamath...

#### Ryan Lahfa (May 30 2020 at 16:39):

Screen-Capture_select-area_20200530183933.png

that was it

#### Ryan Lahfa (May 30 2020 at 16:39):

but it broke the toggle button

#### Patrick Massot (May 30 2020 at 16:40):

I still think the inner list should extend horizontally to fill the container (and there should be no leaf next to them, but this is a yaml content issue)

#### Mario Carneiro (May 30 2020 at 16:41):

Patrick Massot said:

Mario didn't need CSS in metamath...

Interesting that you mention that, just this week we had a conversation about upgrading our HTML validator and the new one yells at us for using <FONT> tags

#### Ryan Lahfa (May 30 2020 at 16:42):

@Patrick Massot I pushed the fix for accordions

#### Ryan Lahfa (May 30 2020 at 16:42):

The thing now is that due to this kind of styling

#### Ryan Lahfa (May 30 2020 at 16:43):

When I hide todo sections, Bootstrap cannot put the border-bottom, because it's in display: hidden and the selector is like "apply the bottom border on the last element in the DOM"

#### Ryan Lahfa (May 30 2020 at 16:43):

I'm not sure I see easy workarounds

#### Ryan Lahfa (May 30 2020 at 16:44):

I'll have to manually force-style the previous element in the section, I'm not sure

#### Ryan Lahfa (May 30 2020 at 16:44):

Anyway, if we can get this PR merged, we can get more improvements later, @Patrick Massot is this okay with you?

#### Patrick Massot (May 30 2020 at 16:46):

Yes, I think this will help people discussing it. Everybody will be able to play with it. Hopefully this will also increase motivation for working on the yaml file.

#### Patrick Massot (May 30 2020 at 16:46):

Everybody, we are discussing https://leanprover-community.github.io/overview.html

#### Patrick Massot (May 30 2020 at 16:47):

This is currently live but without any link pointing towards it.

#### Ryan Lahfa (May 30 2020 at 16:47):

this bottomless stuff is making me crazy

#### Ryan Lahfa (May 30 2020 at 16:47):

Oops @Patrick Massot

I'll fix it…

No

Don't fix it

#### Kevin Buzzard (May 30 2020 at 16:47):

https://mathlib_docs/algebra/char_p.html#frobenius isn't a valid URL

#### Patrick Massot (May 30 2020 at 16:48):

I very carefully checked there was no link to it

#### Kevin Buzzard (May 30 2020 at 16:48):

Why does Fields have fields as a subthing?

#### Patrick Massot (May 30 2020 at 16:48):

We need at least one pass over the whole yaml file before linking to this webpage

#### Ryan Lahfa (May 30 2020 at 16:48):

I meant the fact that mathlib_docs are not pointing correctly is a bug

#### Kevin Buzzard (May 30 2020 at 16:48):

Does "todo" mean "we need to add a link" or "we need to formalise this"?

#### Ryan Lahfa (May 30 2020 at 16:48):

@Kevin Buzzard It means both currently

#### Patrick Massot (May 30 2020 at 16:48):

It currently means either of these

#### Patrick Massot (May 30 2020 at 16:49):

Fields has fields as a subthing because the big one should read "Field theory"

#### Kevin Buzzard (May 30 2020 at 16:49):

So "Distributions on Rd" is not LaTeX'ed up, presumably you know this

#### Ryan Lahfa (May 30 2020 at 16:49):

@Kevin Buzzard Yes, LaTeX-ification is open to improvements :-)

#### Patrick Massot (May 30 2020 at 16:50):

Kevin, it wouldn't take more time to fix it on github than to write it here

#### Kevin Buzzard (May 30 2020 at 16:50):

but of course in general it's a really nice resource.

#### Kevin Buzzard (May 30 2020 at 16:50):

Yeah but I need to go

#### Patrick Massot (May 30 2020 at 16:50):

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

#### Johan Commelin (May 30 2020 at 16:50):

There are commas at the and of the lists. Is that intended?

Unfortunately

#### Ryan Lahfa (May 30 2020 at 16:51):

When the next element is hidden

#### Ryan Lahfa (May 30 2020 at 16:51):

I don't do adjustements to make the comma disappear

#### Kevin Buzzard (May 30 2020 at 16:51):

\"Usual\" functions in single variable real analysis

Ok

#### Patrick Massot (May 30 2020 at 16:51):

If this is all too painful we can still make a different webpage with the todoes

#### Ryan Lahfa (May 30 2020 at 16:51):

Kevin Buzzard said:

\"Usual\" functions in single variable real analysis

That's an easy fix, \ should be dropped in the YAML, it can be edited online

#### Kevin Buzzard (May 30 2020 at 16:52):

I will take a very good look at this on Tues when my deadlines are over

#### Kevin Buzzard (May 30 2020 at 16:52):

There is of course a lot of overlap with https://leanprover-community.github.io/mathlib-overview.html

#### Ryan Lahfa (May 30 2020 at 16:52):

Patrick Massot said:

If this is all too painful we can still make a different webpage with the todoes

I don't think that'd be hard, but it just require that I think about the problem seriously and not implement workarounds on the top of workarounds

#### Johan Commelin (May 30 2020 at 16:52):

We could add "Expand all / Collapse all"

#### Ryan Lahfa (May 30 2020 at 16:52):

Johan Commelin said:

We could add "Expand all / Collapse all"

That's easy to do

#### Johan Commelin (May 30 2020 at 16:52):

Kevin Buzzard said:

There is of course a lot of overlap with https://leanprover-community.github.io/mathlib-overview.html

Yup, but that list was ad hoc. This one has an official "stamp" from French education...

#### Ryan Lahfa (May 30 2020 at 16:53):

Can add it but not right now, I'm hungry

#### Ryan Lahfa (May 30 2020 at 16:53):

Johan Commelin said:

Kevin Buzzard said:

There is of course a lot of overlap with https://leanprover-community.github.io/mathlib-overview.html

Yup, but that list was ad hoc. This one has an official "stamp" from French education...

#### Kevin Buzzard (May 30 2020 at 16:53):

Is it somehow possible to make that mathlib-overview page have the same format I wonder? Do we even want that though, or is the simpler formatting of the overview page better perhaps?

#### Kevin Buzzard (May 30 2020 at 16:53):

For the overview page there is no particular "goal" -- here we have a very well-defined and, in my opinion, extremely exciting, goal.

#### Johan Commelin (May 30 2020 at 16:53):

I think that eventually the two lists should be merged

#### Johan Commelin (May 30 2020 at 16:54):

And we could generate different pages from the same source .yaml file

#### Ryan Lahfa (May 30 2020 at 16:54):

Definitely possible

#### Kevin Buzzard (May 30 2020 at 16:56):

Is it possible to add (not right now, but at some point) more stuff? For example at Imperial they learn Jordan Canonical Form

#### Ryan Lahfa (May 30 2020 at 16:56):

It might be already there implicitly as the french name of "reduction techniques"

#### Ryan Lahfa (May 30 2020 at 16:57):

I don't recall if Jordan is part of agrég

#### Kevin Buzzard (May 30 2020 at 16:57):

I am 100% sure there will one random thing on our curriculum which is not on this list, that's what I'm saying basically

#### Patrick Massot (May 30 2020 at 16:57):

Sure, all this is possible. We can add a page with more advanced stuff, or add more sections

#### Kevin Buzzard (May 30 2020 at 16:57):

or on Cambridge's curriculum or whatever

#### Ryan Lahfa (May 30 2020 at 16:57):

FWIW, https://laurent.claessens-donadello.eu/pdf/lefrido.pdf should represent a decent part of the agrég

#### Patrick Massot (May 30 2020 at 16:57):

I'm pretty sure Jordan is there somewhere, maybe implicitly

But it's French

#### Johan Commelin (May 30 2020 at 16:57):

I think the next step would be to add tags in the list:

Linear Algebra:
Matrices:
Inverse:
tag: [agreg, icl]


Jordan is 9.13

#### Kevin Buzzard (May 30 2020 at 16:58):

OK I'm going back to the treadmill. It looks really nice. I don't really have a feeling for what it will look like on Wednesday when it's complete, but hopefully it looks respectable.

#### Ryan Lahfa (May 30 2020 at 16:58):

Johan Commelin said:

I think the next step would be to add tags in the list:

Linear Algebra:
Matrices:
Inverse:
tag: [agreg, icl]


it requires just minor adjustement in the Python code, but we can very much support it

#### Patrick Massot (May 30 2020 at 16:59):

No Johan, the next step is to finish the first pass on the yaml linkifying

:DDDDDD

#### Johan Commelin (May 30 2020 at 16:59):

Ok, sure. I meant the next next step

#### Patrick Massot (May 30 2020 at 17:01):

Ok, I'll have a go at Section 6: Single variable real analysis.

#### Bryan Gin-ge Chen (May 30 2020 at 17:04):

@Ryan Lahfa I've given you write access to the repo. Also, the CI now builds all branches (except master and oldsite), and deploys only happen for newsite.

#### Patrick Massot (May 30 2020 at 17:07):

Oh crap, the very first item I picked is hard. Topology on R...

#### Patrick Massot (May 30 2020 at 17:07):

R gets its topology as a uniform space

Metric space?

Yes

#### Patrick Massot (May 30 2020 at 17:12):

I linked to real.metric_space

#### Patrick Massot (May 30 2020 at 17:16):

Another tricky one: cluster point of a sequence. Of course we have that as a special case of filter stuff, but do we have a specific definition? If not then I'll let this blank

#### Bryan Gin-ge Chen (May 30 2020 at 17:18):

The underlined links will hopefully be addressed by doc-gen#20. @Ryan Lahfa, are you still around? :smile:

#### Patrick Massot (May 30 2020 at 17:20):

I think he's having dinner.

#### Patrick Massot (May 30 2020 at 17:20):

But I don't understand how a young nerd can have dinner away from his keyboard.

#### Ryan Lahfa (May 30 2020 at 17:22):

Patrick Massot said:

But I don't understand how a young nerd can have dinner away from his keyboard.

That's because my kitchen is not yet integrated!

#### Ryan Lahfa (May 30 2020 at 17:22):

Bryan Gin-ge Chen said:

The underlined links will hopefully be addressed by doc-gen#20. Ryan Lahfa, are you still around? :smile:

I'm around, I still need to do something which is good for everyone :D

#### Ryan Lahfa (May 30 2020 at 17:22):

I can try to move it forward today

#### Ryan Lahfa (May 30 2020 at 17:26):

By curiosity, do we even have distributions in Lean?

#### Patrick Massot (May 30 2020 at 17:29):

Distributions in the sense of Schwartz?

We don't.

#### Patrick Massot (May 30 2020 at 17:32):

@Sebastien Gouezel or @Yury G. Kudryashov do you know whether we have the description of connected subsets of R? The closest I can find is https://leanprover-community.github.io/mathlib_docs/topology/algebra/ordered.html#is_preconnected_iff_forall_Icc_subset

#### Yury G. Kudryashov (May 30 2020 at 17:33):

We don't. We have is_preconnected_iff_forall_Icc_subset and is_preconnected_I??.

#### Yury G. Kudryashov (May 30 2020 at 17:35):

How would you formulate real.is_(pre)connected_iff to make it useful?

#### Patrick Massot (May 30 2020 at 17:38):

I think we could at least say connected iff convex

#### Patrick Massot (May 30 2020 at 17:39):

Do you know whether we have convergent numerical series. I know about has_sum, but this is a stronger notion. I know we can state "partial sums converge", but do we actually have a def?

#### Patrick Massot (May 30 2020 at 17:40):

It's dinner time. See you later

#### Yury G. Kudryashov (May 30 2020 at 17:42):

has_sum uses tendsto (λ n, ∑ i in range n, a i) at_top (nhds s).

#### Yury G. Kudryashov (May 30 2020 at 17:46):

is_preconnected_iff_convex is is_preconnected_iff_forall_Icc_subset.trans convex_real_iff.symm (no, one of them has x≤y)

#### Patrick Massot (May 30 2020 at 17:58):

There are two different has_sum then

Where is yours?

#### Yury G. Kudryashov (May 30 2020 at 18:00):

Sorry, I meant that the file about has_sum uses this tendsto when talking about normal series convergence.

#### Yury G. Kudryashov (May 30 2020 at 18:00):

I should read my messages before sending them.

#### Patrick Massot (May 30 2020 at 18:02):

But we still miss a def here

#### Paul van Wamelen (May 30 2020 at 18:28):

How do I help edit this on github? (without submitting a PR from a fork?)

#### Patrick Massot (May 30 2020 at 18:35):

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml

#### Patrick Massot (May 30 2020 at 18:36):

Do you see the little pen button on the top-right corner?

#### Patrick Massot (May 30 2020 at 18:36):

(I'm asking because I admin rights on this repo, so I'm not 100% sure what is visible by everybody)

#### Patrick Massot (May 30 2020 at 18:37):

Please don't edit Section 6 before I say I'm done with it, otherwise we may duplicate efforts.

#### Paul van Wamelen (May 30 2020 at 18:42):

I see the pen, but because I don't have write permissions it will still create a fork, But I guess that is fine. Can I help with just the styling and some of the English? Top level titles should be all capitals (except for articles and short conjuctions). Next level should at least start with a capital. Others all lower case?

#### Paul van Wamelen (May 30 2020 at 18:44):

I don't see where to edit this, but want to mention: "This page tracks usual mathematical theories that are or not are in mathlib currently" should be "This page tracks usual mathematical theories that are or are not in mathlib currently"

#### Patrick Massot (May 30 2020 at 18:46):

Sorry I misunderstood. Technically it does create a fork, but nothing happens on your hard-drive.

#### Patrick Massot (May 30 2020 at 18:47):

Fixes to the English and styling are welcome of course

#### Paul van Wamelen (May 30 2020 at 18:54):

Did a VERY small PR just to see how it works...

Merged!

#### Patrick Massot (May 30 2020 at 19:09):

I need reviewers for https://github.com/leanprover-community/leanprover-community.github.io/pull/44, especially @Sebastien Gouezel In this PR I also discuss my general ideas about how to work on these links.

#### Patrick Massot (May 30 2020 at 19:17):

I should add that this PR took me a lot more time that I anticipated, but I also learned stuff about mathlib (some items were good surprises whose existence in mathlib was unknown to me).

#### Sebastien Gouezel (May 30 2020 at 19:33):

I am not sure I can see where the threshold is to say we have something. For instance, we don't have a definition of absolutely converging series, but we have the theorem

lemma summable_of_summable_norm {f : ι → α} (hf : summable (λa, ∥f a∥)) : summable f :=
summable_of_norm_bounded _ hf (assume i, le_refl _)


And I don't think we should (ever) define absolutely converging series, since it is just summable (λa, ∥f a∥), and the interesting bit is the above theorem. Does this mean that we will never consider this item as done in mathlib?

#### Patrick Massot (May 30 2020 at 19:40):

As I wrote in the PR, there will always be borderline case. If we think something will never be added then it's a good indication something is wrong. We should then either reformulate the line (or even remove it in extreme cases) or link to something close. In this case, I would agree with you if we had converging series instead of summable families.

#### Patrick Massot (May 30 2020 at 19:41):

I mean I would fill this item with a version of this lemma involving converging series

#### Sebastien Gouezel (May 30 2020 at 19:44):

But this lemma is stronger than the version for converging series, with

lemma has_sum.tendsto_sum_nat {f : ℕ → α} (h : has_sum f a) :
tendsto (λn:ℕ, ∑ i in range n, f i) at_top (𝓝 a)


(in infinite_sum.lean). To me, it only highlights the fact that this curriculum is not optimized for higher-level applications, not a deficiency in mathlib.

#### Patrick Massot (May 30 2020 at 19:47):

Don't you think we should still have a predicate saying that a series converge? And then people will look for the weaker statement (although its proof will use the stronger one)

#### Sebastien Gouezel (May 30 2020 at 19:51):

You mean, give a name to the fact that the partial sums tend to to some limit? I don't really have an opinion on this: it wouldn't hurt but it wouldn't be very useful either, except to say that we have all undergrad maths.

#### Kevin Buzzard (May 30 2020 at 19:53):

Alternatively we could just not fuss and point to something like summable_of_summable_norm and leave it to people to figure out what we mean.

#### Kevin Buzzard (May 30 2020 at 19:54):

One could similarly argue that we'll never have group homomorphisms because we only have monoid homomorphisms

#### Patrick Massot (May 30 2020 at 19:54):

Sure, we can use this link, but the question of converging series still stansd

#### Sebastien Gouezel (May 30 2020 at 19:57):

Same question for positive series. We have a good deal on ennreal and nnreal-valued series in topology/instances/ennreal.lean (notably that an ennreal-valued series always has a sum, that an nnreal-valued one converges if and only if the sum of the ennreal-valued coe is not infinite, and consequences for real-valued series whose terms are all nonnegative. What more could you add?

#### Patrick Massot (May 30 2020 at 20:02):

Of course for positive series there is nothing to add, they converge only when they are summable

#### Patrick Massot (May 30 2020 at 20:03):

Does anyone know the English translation of "Réduction des endomorphismes"?

#### Johan Commelin (May 30 2020 at 20:04):

Context? Analysis?

#### Patrick Massot (May 30 2020 at 20:08):

It's the grab bag where you put the study of eigenvalues, eigenvectors, trigonalization, Jordan normal form etc.

#### Patrick Massot (May 30 2020 at 20:09):

Also, given a matrix A, how would you call a polynomial P such that P(A) = 0?

#### Patrick Massot (May 30 2020 at 20:09):

The yaml file calls it a cancelling polynomial but it sounds fishy to me

#### Bryan Gin-ge Chen (May 30 2020 at 20:10):

I learned it as the characteristic polynomial.

#### Johan Commelin (May 30 2020 at 20:12):

I don't know of a name for such polynomials... but knowing that the minimal polynomial divides them is the only interesting property that they have, right?

#### Alex J. Best (May 30 2020 at 20:12):

Patrick Massot said:

Also, given a matrix A, how would you call a polynomial P such that P(A) = 0?

You mean any polynomial with that property? We have minimal polynomial for the smallest one and characteristic for det(x-A) but otherwise no name for this.

#### Patrick Massot (May 30 2020 at 20:12):

Yes any polynomial

#### Bryan Gin-ge Chen (May 30 2020 at 20:13):

Right, I misread. I agree with Alex.

#### Patrick Massot (May 30 2020 at 20:13):

It feels completely crazy that you don't have a name for this. I need to rethink everything I know about linear algebra to try to express it without this word.

#### Patrick Massot (May 30 2020 at 20:14):

Does anyone has a translation?

#### Patrick Massot (May 30 2020 at 20:15):

I need a header for the following list:

    eigenvalue: ''
eigenvector: ''
diagonalization: ''
trigonalization: ''
endomorphism invariant subspaces: ''
characteristic subspaces: ''
kernel lemma: ''
Dunford decomposition: ''
Jordan normal form: ''


#### Bryan Gin-ge Chen (May 30 2020 at 20:15):

Patrick Massot said:

Finite-dimensional spectral theory?

#### Patrick Massot (May 30 2020 at 20:15):

By the way, the translation "kernel lemma" also sounds fishy

#### Alex J. Best (May 30 2020 at 20:15):

Patrick Massot said:

It feels completely crazy that you don't have a name for this. I need to rethink everything I know about linear algebra to try to express it without this word.

If I had to make one up annihilating polynomial sounds more natural.

#### Johan Commelin (May 30 2020 at 20:16):

Patrick Massot said:

By the way, the translation "kernel lemma" also sounds fishy

What does it mean?

#### Alex J. Best (May 30 2020 at 20:16):

Hmm it seems this term is used https://www.maths.ed.ac.uk/~tl/minimal.pdf

#### Patrick Massot (May 30 2020 at 20:16):

https://fr.wikipedia.org/wiki/Lemme_des_noyaux

#### Johan Commelin (May 30 2020 at 20:17):

Nope... the only other place on earth where such a lemma exists is in Catalan...

#### Patrick Massot (May 30 2020 at 20:17):

annihilating polynomial is the direct translation of the French name, I like it

#### Patrick Massot (May 30 2020 at 20:17):

Seriously, Johan, didn't you study linear algebra?

#### Johan Commelin (May 30 2020 at 20:18):

Not really... actually. I skipped all the lectures.

#### Bryan Gin-ge Chen (May 30 2020 at 20:18):

Hmm, a comment on this math stackexchange page suggests "primary decomposition": https://math.stackexchange.com/questions/3077162/name-for-the-kernel-lemma

#### Patrick Massot (May 30 2020 at 20:21):

So we need to prove this in mathlib. Then people will see this strange name "kernels lemma" and click the link to start learning linear algebra properly.

#### Patrick Massot (May 30 2020 at 20:23):

I see there is a "unitary ring" line. Do we plan to have non-unital rings in mathib at some point?

#### Johan Commelin (May 30 2020 at 20:25):

I wouldn't know the axioms... mul_assoc? But not has_one?

#### Patrick Massot (May 30 2020 at 20:26):

https://en.wikipedia.org/wiki/Ring_(mathematics)#Multiplicative_identity:_mandatory_vs._optional

#### Paul van Wamelen (May 30 2020 at 20:27):

I submitted another PR

#### Johan Commelin (May 30 2020 at 20:28):

We have noncommutative rings in mathlib... isn't that good enough?

#### Patrick Massot (May 30 2020 at 20:29):

Crap, this PR is super conflicting what I was doing

#### Paul van Wamelen (May 30 2020 at 20:31):

I can try and "hand merge" it... Gimme a sec.

#### Patrick Massot (May 30 2020 at 20:32):

There is no conflict on GitHub. It conflicts my open PR and my local modifications. But it's ok, I'll handle it.

#### Patrick Massot (May 30 2020 at 20:32):

Let's do both actually: I'll my merge my PR and you'll fix yours

#### Patrick Massot (May 30 2020 at 20:33):

And then I'll fix conflicts with my local changes

#### Patrick Massot (May 30 2020 at 20:33):

Done. Now you have conflicts

#### Kevin Buzzard (May 30 2020 at 20:39):

https://fr.wikipedia.org/wiki/D%C3%A9composition_de_Dunford -- this is the first time I've seen the French choose to name some lemma after someone who isn't French, when there was a perfectly good French option (décomposition de Jordan-Chevalley)

#### Patrick Massot (May 30 2020 at 20:40):

And how do you say "réduction des endomorphismes"?

#### Reid Barton (May 30 2020 at 20:41):

Is this "structure theory of endomorphisms"?

#### Reid Barton (May 30 2020 at 20:41):

I guess that's kind of a mixed metaphor

#### Paul van Wamelen (May 30 2020 at 20:45):

I think I cleared the conflicts

Awesome.

#### Ryan Lahfa (May 30 2020 at 20:53):

Patrick Massot said:

It feels completely crazy that you don't have a name for this. I need to rethink everything I know about linear algebra to try to express it without this word.

My whole problem, I even warned about it before :D

#### Ryan Lahfa (May 30 2020 at 20:54):

Hahahaha, this thread has really turned into how does you say X in english :'D

#### Kenny Lau (May 30 2020 at 20:55):

what a surprise, a second language is not just the first language plus a dictionary

#### Scott Morrison (May 30 2020 at 20:57):

I think we'll eventually want non-unital rings, sadly. For example you might want continuous functions vanishing at infinity on a locally compact space as a non-unital algebra, to state the version of Stone-Weierstrass for locally compact spaces.

#### Patrick Massot (May 30 2020 at 20:58):

I just pushed some beginning of structure cleanup, but I need to go. Everybody should feel free to work on this file, I won't touch it in the next 10 hours.

#### Ryan Lahfa (May 30 2020 at 21:02):

Kenny Lau said:

what a surprise, a second language is not just the first language plus a dictionary

But it's surprising for cancelling/annihilating polynomials to not have any equivalent, like while I was learning linear algebra, this term was pronounced like 30 times per day during exercises

#### Ryan Lahfa (May 30 2020 at 21:02):

And same goes for many terms I guess

#### Alex J. Best (May 30 2020 at 21:06):

I think we just got away with let $P$ be a polynomial s.t. $P(M) = 0$, as its not really longer to say the full definition in this case!

#### Ryan Lahfa (May 30 2020 at 21:14):

Alex J. Best said:

I think we just got away with let $P$ be a polynomial s.t. $P(M) = 0$, as its not really longer to say the full definition in this case!

Yes but sometimes you want to say things like
"Method to compute $\exp(M)$ when you have a $P$ such that $P(M) = 0$"
vs
"Method to compute $\exp(M)$ using an annhilating polynomial"

#### Ryan Lahfa (May 30 2020 at 21:15):

Anyway, I'm getting sidetracked… :D

#### Kevin Buzzard (May 30 2020 at 21:26):

Hecke algebras are something which will be within reach soon, and they're rings without 1

#### Johan Commelin (Jun 01 2020 at 09:01):

#5 is about affine spaces. I'm kicking #2816 on the merge queue. Once it lands, we can fill out this section. @Joseph Myers please let us know if you would like to contribute.

#### Johan Commelin (Jun 01 2020 at 09:02):

@Oliver Nash and/or @Anne Baanen Would you mind filling out #4 on bilinear and quadratic forms?

#### Johan Commelin (Jun 01 2020 at 09:03):

If any of you doesn't have time/energy/interest in contributing, just say so. No hard feelings.

#### Johan Commelin (Jun 01 2020 at 09:06):

#7 is on single variable complex analysis, and it's going to make us look ridiculous...

#### Johan Commelin (Jun 01 2020 at 09:08):

I'll start on #8. Topology now.

#### Patrick Massot (Jun 01 2020 at 09:09):

Maybe it would make more sense to work on an algebraic section since I would have an easier time doing topology than algebra

#### Johan Commelin (Jun 01 2020 at 09:12):

The first item is interesting. We don't have metric_space.to_topological_space I guess. So what do we do? metric_space.to_uniform_space?

#### Patrick Massot (Jun 01 2020 at 09:15):

I found rather link a lemma saying something is open if it contains an open ball around each point, or something like that

Aha, makes sense

#### Johan Commelin (Jun 01 2020 at 09:17):

The remaining sections are:

#09. Differential Calculus
#10. Integral Calculus
#11. Probability Theory
#12. Distribution calculus
#13. Numerical Analysis


I fear that the last 3 will stay empty.

#### Patrick Massot (Jun 01 2020 at 09:18):

Don't we have at least the definition of a probability measure?

#### Johan Commelin (Jun 01 2020 at 09:19):

pmf ­– Probability mass function

#### Johan Commelin (Jun 01 2020 at 09:19):

But otherwise, not much, I think

#### Oliver Nash (Jun 01 2020 at 09:24):

Johan Commelin said:

Oliver Nash and/or Anne Baanen Would you mind filling out #4 on bilinear and quadratic forms?

I would be delighted to fill this out. I'll try and find time this evening though it might not happen till tomorrow.

#### Patrick Massot (Jun 01 2020 at 09:24):

Don't hesitate to reorder and slightly reword stuff if it makes more sense.

#### Oliver Nash (Jun 01 2020 at 09:24):

Thanks, will do. Needless to say I'm happy for @Anne Baanen to do this too / instead.

#### Patrick Massot (Jun 01 2020 at 09:25):

Also keep in mind the structure is not yet fully compliant. We want to have exactly three levels: main heading, sub heading, leaf containing a link.

#### Oliver Nash (Jun 01 2020 at 09:25):

Understood, I will stick to a three-level structure.

#### Johan Commelin (Jun 01 2020 at 09:26):

Thanks for helping!

My pleasure!

#### Johan Commelin (Jun 01 2020 at 09:33):

https://github.com/leanprover-community/leanprover-community.github.io/pull/48 fills links in basic topology (there's a lot left for the experts :wink:)

#### Johan Commelin (Jun 01 2020 at 09:35):

Note: affine spaces have been merged

#### Patrick Massot (Jun 01 2020 at 09:36):

Ok, I merged but indeed we have several more links to add to this section. I'll do it right now

#### Patrick Massot (Jun 01 2020 at 09:38):

Each time I type leanproject up in mathlib, elan downloads something... :grinning:

#### Patrick Massot (Jun 01 2020 at 10:09):

Why can't I find that a real normed space is finite-dimensional iff the unit ball is compact? Is it really missing?

#### Patrick Massot (Jun 01 2020 at 10:15):

I've updated the metric topology section.

#### Sebastien Gouezel (Jun 01 2020 at 10:24):

The useful implication is there (finite_dimensional.proper). The useless implication has been done by a student of Kevin, if I recall correctly, but it never made it into mathlib.

#### Kevin Buzzard (Jun 01 2020 at 10:25):

https://github.com/LAC1213/compact_unit_ball

#### Patrick Massot (Jun 01 2020 at 10:28):

Ok, so I can't really tick that one off. Too bad this project never went to mathlib...

#### Ryan Lahfa (Jun 01 2020 at 10:34):

Patrick Massot said:

Ok, so I can't really tick that one off. Too bad this project never went to mathlib...

If there was a license, this could be salvaged

#### Patrick Massot (Jun 01 2020 at 10:34):

I'm pretty sure you can discuss this with the author. That would be a nice little project.

#### Patrick Massot (Jun 01 2020 at 10:35):

Of course turning this into something PRable means work.

#### Patrick Massot (Jun 01 2020 at 10:35):

But it would be a nice way to get familiar with both linear algebra and topology in mathlib.

#### Sebastien Gouezel (Jun 01 2020 at 10:40):

If I remember correctly, there is the useless assumption that the field is complete in this project, but this is not crazy to have this assumption.

#### David Wärn (Jun 01 2020 at 10:57):

Shouldn't this argument be phrased using docs#riesz_lemma ?

#### Patrick Massot (Jun 01 2020 at 11:09):

Indeed it looks like someone started this road but gave up.

#### Patrick Massot (Jun 01 2020 at 11:10):

It seems to be Jean. @Jean Lo what is the status of this?

#### Joseph Myers (Jun 01 2020 at 11:47):

What I defined for affine spaces is very minimal at present, so there won't be much from that list (on the Euclidean side, I suppose #2865 provides at least "Angles of vectors"). It's not yet PRed, but I do have the result that (not necessarily bijective) isometries between Euclidean affine spaces are affine maps that preserve the inner product (the list wants rather more about isometries than that, however).

#### Johan Commelin (Jun 01 2020 at 11:58):

@Joseph Myers Sure... but all small bits help.

#### Patrick Massot (Jun 01 2020 at 12:13):

Joseph, did you coordinate with https://leanprover-community.github.io/mathlib_docs/analysis/normed_space/mazur_ulam.html?

#### Johan Commelin (Jun 01 2020 at 12:25):

Is "C is algebraically closed" somewhere on the agreg list?

I hope so

#### Patrick Massot (Jun 01 2020 at 13:53):

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml#L183

#### Joseph Myers (Jun 01 2020 at 15:13):

@Patrick Massot No, I just wrote a separate proof (for Euclidean spaces, the (easy) result isn't limited to bijective isometries, and the "preserves inner product" part is something useful for describing the effect of an isometry (from a finite-dimensional space to itself) on coordinates, once a frame has been chosen, as the combination of an orthogonal matrix and a translation).

#### Yury G. Kudryashov (Jun 01 2020 at 15:15):

Actually, you don't need a Euclidean space here. Only a normed_add_torsor over a normed_vector_space with strictly convex balls.

#### Yury G. Kudryashov (Jun 01 2020 at 15:20):

Actually you can prove the following fact. Let f be an isometry, and its codomain is a normed_add_torsor R E such that 0 < r → dist x y = r → dist x z = r → r < dist x (2 * y - z). Then f is affine.

#### Johan Commelin (Jun 01 2020 at 15:22):

Patrick Massot said:

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml#L183

I've never heard of this name before...

#### Joseph Myers (Jun 01 2020 at 15:24):

Feel free to add these more general results! I think for isometries of Euclidean spaces there should be a function mapping f (such that isometry f) to an affine_map (for whatever type classes that include the case of Euclidean spaces), and a proof that the corresponding linear_map preserves the inner product, but I'm not particularly concerned with how we get there.

#### Yury G. Kudryashov (Jun 01 2020 at 15:27):

BTW, do you prove that for an affine isometry the corresponding linear_map is an isometry as well?

#### Ryan Lahfa (Jun 01 2020 at 15:28):

Johan Commelin said:

Patrick Massot said:

https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml#L183

I've never heard of this name before...

https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_fondamental_de_l%27alg%C3%A8bre
That's the name we give it, maybe we love too much to give names to theorem.
I even heard that the fact that the continuous image of a compact is a compact is called Weierstrass' theorem :D in France…

#### Yury G. Kudryashov (Jun 01 2020 at 15:29):

English Wikipedia never mentions this name, just "Fundamental theorem of algebra"

#### Ryan Lahfa (Jun 01 2020 at 15:30):

That's an invitation to change the name into "fundamental theorem of algebra" I believe

#### Yury G. Kudryashov (Jun 01 2020 at 16:08):

https://github.com/leanprover-community/leanprover-community.github.io/commit/bebb1e9cafaee64414639bc9714f09d9b124ca0f

#### Patrick Massot (Jun 01 2020 at 16:25):

Some algebraists will hate you Yury. I know more than one that is really pissed off when an analysis theorem is called the "fundamental theorem of algebra".

#### Kevin Buzzard (Jun 01 2020 at 16:27):

It's because algebra := polynomials and matrices in 1800 or something, right?

#### Yury G. Kudryashov (Jun 01 2020 at 17:00):

@Patrick Massot Is there a title that is both widely recognizable (in English) and won't make algebraists hate me?

#### Johan Commelin (Jun 01 2020 at 17:02):

The algebraists should be happy that they have opportunity to invade the territory of the analysts!
Geometers don't even have a "fundamental theorem".... look at them :stuck_out_tongue_wink:

#### Patrick Massot (Jun 01 2020 at 17:55):

The title could be "$\mathbb C$ is algebraically closed"...

#### Johan Commelin (Jun 01 2020 at 17:56):

Such a boring theorem name... you've been influenced too much by mathlib naming conventions.

#### Patrick Massot (Jun 01 2020 at 17:58):

I can see you don't know what this theorem is called in mathlib...

#### Johan Commelin (Jun 01 2020 at 17:58):

polynomial.complex_exists_root?

#### Johan Commelin (Jun 01 2020 at 17:58):

That's just because we don't have class algebraically_closed (K : Type*) [field K] yet.

#### Johan Commelin (Jun 01 2020 at 17:59):

Otherwise it would be complex.algebraically_closed.

#### Joseph Myers (Jun 01 2020 at 20:01):

@Yury G. Kudryashov I didn't prove that particular result that the corresponding linear_map is an isometry, but it's a straightforward consequence of the other facts in this area.

E.g., from #2907

#### Joseph Myers (Jun 02 2020 at 01:09):

Actually it's true more generally than that, for the map (at a particular base point) on vectors induced by any isometry between two normed_add_torsors. Does this belong in mathlib?

import analysis.normed_space.add_torsor
import topology.metric_space.isometry

variables (V1 : Type*) {P1 : Type*} [normed_group V1] [metric_space P1] [normed_add_torsor V1 P1]
variables (V2 : Type*) {P2 : Type*} [normed_group V2] [metric_space P2] [normed_add_torsor V2 P2]

/-- The map on vectors corresponding to a map from P1 to P2, at a base
point p. -/
def vector_map_of_point_map (f : P1 → P2) (p : P1) : V1 → V2 := λ v, f (v +ᵥ p) -ᵥ f p

/-- The map described by vector_map_of_point_map is an isometry if
the original map is one. -/
lemma isometry_vector_map_of_point_map {f : P1 → P2} (h : isometry f) (p : P1) :
isometry (vector_map_of_point_map V1 V2 f p) :=
begin
rw isometry_emetric_iff_metric at *,
unfold vector_map_of_point_map,
intros x y,
convert h (x +ᵥ p) (y +ᵥ p),
end


#### Johan Commelin (Jun 02 2020 at 04:42):

@Joseph Myers I think it does, but I wouldn't make a new definition. (Or at least, don't use the definition in the lemma. Rather, take any random map g : V1 → V2 and the hypothesis hg : \forall v, g v = f (v +ᵥ p) -ᵥ f p. In this way, the lemma will also be applicable to maps that aren't definitionally a vector_map_of_point_map. My intuition says that is what will happen in practice.

#### Yury G. Kudryashov (Jun 02 2020 at 05:04):

Note that with #2907 you can represent your map as a composition of known isometries, and get the proof from isometry.comp.

#### Yury G. Kudryashov (Jun 02 2020 at 05:05):

Probably we should stop hijacking Patrick's thread.

#### Johan Commelin (Jun 02 2020 at 08:54):

@Ryan Lahfa There's something wrong with the statement-todo and statement-done classes. Currently cards are also getting these classes, but not in an intuitive way.

#### Johan Commelin (Jun 02 2020 at 08:54):

I think a card should only be marked statement-done if all of its children are completely done.

#### Johan Commelin (Jun 02 2020 at 08:54):

Otherwise our todo-list is much too optimistic.

#### Johan Commelin (Jun 02 2020 at 08:57):

image.png
This doesn't really look as I would expect. The todo toggle seems to be inverted...

#### Johan Commelin (Jun 02 2020 at 08:57):

I'm seeing todo's but the toggle is off, and when I switch it on, the items that are not links go away

#### Ryan Lahfa (Jun 02 2020 at 09:20):

Johan Commelin said:

Ryan Lahfa There's something wrong with the statement-todo and statement-done classes. Currently cards are also getting these classes, but not in an intuitive way.

There might be a bug

#### Ryan Lahfa (Jun 02 2020 at 09:21):

I'll look into it

Thanks!

#### Johan Commelin (Jun 02 2020 at 09:21):

Alternative: strip out the classes and generate two files...

#### Ryan Lahfa (Jun 02 2020 at 09:21):

Johan Commelin said:

I'm seeing todo's but the toggle is off, and when I switch it on, the items that are not links go away

I think it's also due to the fact you don't want to show parts when they are empty (e.g. all children are todos), but I'm not sure, I'll look at it again

Hahahaha

#### Johan Commelin (Jun 02 2020 at 09:22):

Let's just make sure that the list works for the IAS talk, and then we can add the fancy buttons afterwards.

#### Ryan Lahfa (Jun 02 2020 at 09:23):

Agreed ; if I don't find a trivial solution quickly enough, I'll send directly a PR to produce two files, sounds good?

#### Kevin Buzzard (Jun 02 2020 at 09:47):

So I'm having a look at the current state of this (the yaml file). For "direct sum" (line 12) we have the unnamed instance direct_sum.semimodule. This is an "external direct sum". From the context of the list it looks like an internal direct sum though, i.e. a sum of two submodules within a big module, where the submodules happen to have trivial intersection. Should we just not care and link to the external direct sum? And can one link to an unnamed instance name?

#### Johan Commelin (Jun 02 2020 at 09:48):

Internal direct sum = sup in the lattice semimodule _ _??

#### Kevin Buzzard (Jun 02 2020 at 09:48):

It's no different to internal sum though

#### Johan Commelin (Jun 02 2020 at 09:50):

internal direct sum is an awkard notion, where you want to know that things are orthogonal, and then take a sup.

#### Kevin Buzzard (Jun 02 2020 at 09:51):

I remember learning this as an UG too. I think the idea is that abstract direct sum of two vector spaces is supposed to be too difficuilt, and this internal direct sum -- if V and W are subspaces of some large vector space X and V and W intersect trivially, then the space spanned by V and W satisfies the universal property of the abstact direct sum -- was taught first.

#### Johan Commelin (Jun 02 2020 at 09:51):

We just totalise the function...

#### Johan Commelin (Jun 02 2020 at 09:51):

And define it for non-othogonal submodules as well

#### Patrick Massot (Jun 02 2020 at 09:58):

The idea is to find a good entry point for people that may not know much about formalization, but want to use this notion. Sometimes the best entry point for a definition is actually a lemma saying that some funny mathliby way of doing stuff is giving you the expected behavior.

Merged!

#### Patrick Massot (Jun 02 2020 at 10:18):

But I'll probably need to fix structure

#### Kevin Buzzard (Jun 02 2020 at 10:19):

Did I do something wrong? Let me know now because I'm about to start on affine spaces

#### Kevin Buzzard (Jun 02 2020 at 10:19):

And I didn't know how to check if the links work.

#### Kevin Buzzard (Jun 02 2020 at 10:19):

(e.g. I might have missed a namespace)

#### Patrick Massot (Jun 02 2020 at 10:22):

Patrick Massot said:

Don't hesitate to reorder and slightly reword stuff if it makes more sense.

Also keep in mind the structure is not yet fully compliant. We want to have exactly three levels: main heading, sub heading, leaf containing a link.

#### Patrick Massot (Jun 02 2020 at 10:22):

Hold on for two minutes

#### Patrick Massot (Jun 02 2020 at 10:27):

That's what I call "fixing structure", following the guidelines quoted above.

#### Kevin Buzzard (Jun 02 2020 at 10:27):

I see, so actually changing the structure of the yaml to be a bit more sane

#### Kevin Buzzard (Jun 02 2020 at 10:28):

keep precisely the same leaves but we can move them around a bit

#### Patrick Massot (Jun 02 2020 at 10:28):

Yes. Actually I'm pretty disappointed by the source document. I thought it was more structured.

#### Kevin Buzzard (Jun 02 2020 at 10:28):

it probably wasn't written by a computer scientist!

#### Patrick Massot (Jun 02 2020 at 10:29):

Sometimes I even change leaves a bit (and I added Jordan normal form). But the main point is that leaves should be at level 3.

#### Patrick Massot (Jun 02 2020 at 10:29):

https://en.wikipedia.org/wiki/Triple_product

#### Patrick Massot (Jun 02 2020 at 10:29):

Oh, the preceding line is a wrong translation

#### Patrick Massot (Jun 02 2020 at 10:30):

"vector product" means cross product

#### Johan Commelin (Jun 02 2020 at 10:30):

I'm learning new stuff everyday...

#### Patrick Massot (Jun 02 2020 at 10:30):

But we call it "produit vectoriel" in French.

#### Kevin Buzzard (Jun 02 2020 at 10:30):

We don't have any of these crazy things which assume finite-dimensionality (or in this case 3-dimensionality)

#### Patrick Massot (Jun 02 2020 at 10:30):

The triple product thins is about computing determinants using the Euclidean structure

3 is overrated

#### Patrick Massot (Jun 02 2020 at 10:31):

That's why I named this section "low dimensions"

#### Kevin Buzzard (Jun 02 2020 at 10:31):

why not just call it n-ary product and link to det :-)

#### Patrick Massot (Jun 02 2020 at 10:31):

The fact that you can compute determinants using the Euclidean structure has some content

#### Patrick Massot (Jun 02 2020 at 10:32):

But I wouldn't say this has super high priority, unless you specifically work towards low-hanging fruits in this list

#### Ryan Lahfa (Jun 02 2020 at 10:45):

Kevin Buzzard said:

We don't have any of these crazy things which assume finite-dimensionality (or in this case 3-dimensionality)

That's for people who does physics

#### Patrick Massot (Jun 02 2020 at 10:51):

I thought physics was all about dimension 4.

I thought 10?

#### Ryan Lahfa (Jun 02 2020 at 11:07):

Sometimes they forget about time and wrapped dimensions, :-°

#### Johan Commelin (Jun 02 2020 at 13:15):

@Yury G. Kudryashov Didn't you do stuff on Grönwell in mathlib at some point? I can't find it.

#### Yury G. Kudryashov (Jun 02 2020 at 13:16):

https://leanprover-community.github.io/mathlib_docs/analysis/ODE/gronwall.html

Thanks!

#### Johan Commelin (Jun 02 2020 at 13:21):

We don't really have a definition of a sigma algebra :expressionless:

#### Yury G. Kudryashov (Jun 02 2020 at 13:22):

We have [measurable α]

#### Johan Commelin (Jun 02 2020 at 13:24):

Yup... it's just that the name isn't recognisable

#### Johan Commelin (Jun 02 2020 at 13:30):

I've filled in a couple more links in analysis and measure theory. The part on integration I didn't really touch... I've never used that part of the library.

#### Sebastien Gouezel (Jun 02 2020 at 13:35):

A sigma algebra is exactly an instance of measurable_space α

#### Johan Commelin (Jun 02 2020 at 13:40):

It's just that the list has 'measureable spaces' and 'sigma algebras' as seperate items :expressionless:

#### Reid Barton (Jun 02 2020 at 13:42):

We also have measurable spaces https://github.com/leanprover-community/mathlib/blob/master/src/measure_theory/category/Meas.lean#L31 :upside_down:

#### Gabriel Ebner (Jun 02 2020 at 13:43):

What is the difference between a measurable space and a set with a sigma algebra?

#### Reid Barton (Jun 02 2020 at 13:46):

Those are the same, the issue is that (by analogy with group, etc.) the structure measurable_space is named after the bundled concept, when it actually is the unbundled one. Same with topological_space.

#### Johan Commelin (Jun 02 2020 at 13:51):

We really need this automated "rename declarations" bot, that will just go through the entire source to rename things while I sleep.

#### Patrick Massot (Jun 02 2020 at 13:55):

Thanks Johan. Some items are wrong and a lot are missing but it still helps. I'll merge it and improve it.

#### Reid Barton (Jun 02 2020 at 13:56):

FWIW I'm not suggesting renaming the mathlib definitions, just explaining why they don't exactly align with the math names: basically because we don't really use the bundled objects so we have just one name for both "measurable space" and "sigma-algebra".

#### Patrick Massot (Jun 02 2020 at 14:02):

I think the module docstring of https://leanprover-community.github.io/mathlib_docs/measure_theory/measure_space.html could be easier to read...

#### Sebastien Gouezel (Jun 02 2020 at 14:09):

Ah, this is a docstring from the ancient times!

#### Patrick Massot (Jun 02 2020 at 14:09):

Sébastien, do you know whether counting measures are hidden somewhere?

#### Patrick Massot (Jun 02 2020 at 14:10):

And non-discrete probability measures?

#### Sebastien Gouezel (Jun 02 2020 at 14:33):

The counting measure is in measure_space.lean

/-- Counting measure on any measurable space. -/
def count : measure α := sum dirac


#### Johan Commelin (Jun 02 2020 at 14:37):

Patrick Massot said:

Thanks Johan. Some items are wrong and a lot are missing but it still helps. I'll merge it and improve it.

Sorry for the mistakes

#### Patrick Massot (Jun 02 2020 at 14:39):

Oh, I should have checked here before pushing, I missed Sébastien's message.

#### Johan Commelin (Jun 02 2020 at 14:41):

You can push again... it's free.

Done

#### Patrick Massot (Jun 02 2020 at 14:42):

@Sebastien Gouezel would you mind going over https://github.com/leanprover-community/leanprover-community.github.io/blob/c2631dcdfe279ebe5869eb62e6289a6e7d426681/data/overview.yaml#L505-L585 to tell us if we missed stuff?

#### Sebastien Gouezel (Jun 02 2020 at 14:47):

Monotone convergence is lintegral_supr_ae in integration.lean.

#### Sebastien Gouezel (Jun 02 2020 at 14:48):

Fatou is lintegral_liminf_le in integration.lean.

#### Sebastien Gouezel (Jun 02 2020 at 14:49):

By the way, just before Fatou there are the two lines

-- for some reason the next proof fails without changing the priority of this instance
local attribute [instance, priority 1000] classical.prop_decidable


It won't be a surprise to anyone that, with current awesome Lean, they can be safely removed.

#### Patrick Massot (Jun 02 2020 at 14:51):

I just skipped that file because it seems to be all about the mysterious ∫⁻. Isn't there a version for actual integrals?

#### Sebastien Gouezel (Jun 02 2020 at 14:57):

The usual textbook versions of these theorems are for nonnegative functions that are allowed to take the value $+\infty$, so they really talk about the ∫⁻. I just checked in Rudin, for instance, and both monotone convergence and Fatou's lemma are just given in this version.

#### Patrick Massot (Jun 02 2020 at 14:59):

Thanks. We really need some md file describing how to navigate that part of mathlib.

#### Johan Commelin (Jun 02 2020 at 15:00):

Well, a yaml file is a good first start (-;

#### Patrick Massot (Jun 02 2020 at 15:01):

The YaML file doesn't explain what this crazy ∫⁻ symbol means

#### Patrick Massot (Jun 02 2020 at 15:03):

Sébastien, since you're clearly not working on this referee report, would you mind handling Section 9?

#### Patrick Massot (Jun 02 2020 at 15:03):

https://github.com/leanprover-community/leanprover-community.github.io/edit/newsite/data/overview.yaml

#### Sebastien Gouezel (Jun 02 2020 at 15:03):

I got through the interesting part of the paper, now it's the boring technical part, so any excuse for procrastination is good. I'll have a look.

#### Patrick Massot (Jun 02 2020 at 15:05):

At this stage you can write to the editor: I think the theorem is interesting and the new ideas are nice, now I'm waiting for the formalization of the technical details.

#### Sebastien Gouezel (Jun 02 2020 at 15:13):

People still need to get their paper published in a reasonable amount of time, especially if they're young. I could do this when I refer papers whose authors are all tenured :)

#### Johan Commelin (Jun 02 2020 at 15:14):

If that catches on, you'll find authors scrambling for getting a phd student or postdoc as coauthor

#### Patrick Massot (Jun 03 2020 at 18:14):

@Ryan Lahfa since you didn't fix the bugs quickly enough for my talk, I went ahead and split the display into two files. I also added a link.

#### Patrick Massot (Jun 03 2020 at 18:15):

I also cleaned up the remaining sections so that the structure should be consistent now. I'm convinced there are still missing links, but people should now track them by comparing https://leanprover-community.github.io/undergrad_todo.html with what they think is in mathlib.

#### Sebastien Gouezel (Jun 03 2020 at 18:42):

Patrick Massot said:

Ryan Lahfa since you didn't fix the bugs quickly enough for my talk, I went ahead and split the display into two files. I also added a link.

How did the talk go, by the way?

#### Johan Commelin (Jun 03 2020 at 18:43):

It's at 1200 tonight

#### Johan Commelin (Jun 03 2020 at 18:43):

So around 1215, Patrick is going to demo Zulip, and we should all be making silly jokes

#### Gabriel Ebner (Jun 03 2020 at 18:43):

I'm sorry the widgets didn't make it in time for the talk, but the vscode extension still has some rough edges and Ed is a bit busy at the moment.

#### Gabriel Ebner (Jun 03 2020 at 18:44):

@Johan Commelin Which timezone?

#### Johan Commelin (Jun 03 2020 at 18:46):

Midnight in Amsterdam, Paris, Berlin

#### Johan Commelin (Jun 03 2020 at 18:46):

I think it's 1800 Princeton time

#### Gabriel Ebner (Jun 03 2020 at 18:47):

So in 3 hours, i.e. 24:00? I was confused by the 12.

#### Patrick Massot (Jun 03 2020 at 18:47):

It's getting dangerously close.

#### Reid Barton (Jun 03 2020 at 18:47):

I see 5:30 pm on the IAS website which I assume is US/Eastern

Yes, 3 hours

#### Patrick Massot (Jun 03 2020 at 18:47):

5:30 is the beginning of discussions, but the talk starts half an hour later.

#### Patrick Massot (Jun 03 2020 at 18:47):

It's a crazy format.

#### Reid Barton (Jun 03 2020 at 18:48):

Interesting idea to discuss the talk before it happens

#### Patrick Massot (Jun 03 2020 at 18:48):

I replaces a very informal seminar featuring wine and cheese.

#### Patrick Massot (Jun 03 2020 at 18:48):

Before the talk peoples are randomly distributed in Zoom rooms with 6 participants.

#### Patrick Massot (Jun 03 2020 at 18:49):

Then there is the talk and then general discussion.

#### Kevin Buzzard (Jun 03 2020 at 20:23):

We had this with my OWLS talk and it worked really well, but we did it after not before.

#### Patrick Massot (Jun 04 2020 at 00:21):

The talk went fine, discussion just stopped (almost two hours after the talk stopped).

#### Johan Commelin (Jun 04 2020 at 14:55):

#2946 Eisenstein criterion (thanks @Chris Hughes :tada: ) is on the merge queue.

#### Johan Commelin (Jun 04 2020 at 14:55):

So we can update this yaml in a moment (-;

#### Johan Commelin (Jun 04 2020 at 15:28):

@Patrick Massot @Bryan Gin-ge Chen What do you think of hosting things like overview.yaml in mathlib? Then PRs that add new stuff can also add it to that file directly.

#### Johan Commelin (Jun 04 2020 at 15:29):

(And it makes it easier for a reviewer to say: Hey, please update that file as well.)

#### Patrick Massot (Jun 04 2020 at 15:40):

Of course I don't have anything against that. I don't know what would be the best strategy. Maybe the website CI could simply download the file from mathlib before running the site building script.

#### Bryan Gin-ge Chen (Jun 04 2020 at 15:41):

I think it's probably a good idea. Moving overview.yaml to mathlib will change an informal dependency (we have to remember to make changes in two repos) to a technical one (rebuilding the website will require wget from mathlib github as Patrick says).

#### Johan Commelin (Jun 04 2020 at 15:41):

Yup, that's the kind of thing I was meaning

#### Johan Commelin (Jun 04 2020 at 15:41):

Same applies to 100.yaml

#### Johan Commelin (Jun 04 2020 at 15:41):

And stacks.yaml, when we ever get there (-;

#### Patrick Massot (Jun 04 2020 at 15:42):

The case of 100.yaml is slightly different because it also lists stuff from outside mathlib

#### Johan Commelin (Jun 04 2020 at 15:43):

But only very little right? Even archive/ is in the mathlib repo

#### Johan Commelin (Jun 04 2020 at 15:43):

So it's only CH that is outside, I think.

#### Patrick Massot (Jun 04 2020 at 15:44):

We also have more polishing work to be done on this list stuff. We only have the minimal version. We need to get a better idea about interaction between this list and https://leanprover-community.github.io/mathlib-overview.html.

#### Patrick Massot (Jun 04 2020 at 15:45):

One option is to rename overview.yaml into undergrad.yaml, create a file advanced_topics.yaml for everything else, and start by porting whatever is list in the overview page but not in the undergrad page to this new file.

#### Patrick Massot (Jun 04 2020 at 15:46):

The border between undergrad and the rest is pretty blurry, but I think it's interesting anyway.

#### Patrick Massot (Jun 04 2020 at 15:46):

Because it allows to also have https://leanprover-community.github.io/undergrad_todo.html which would not make sense with an open ended scope.

#### Patrick Massot (Jun 04 2020 at 15:47):

Also note that I don't have anything against resurrecting the switches gathering stuff and todo stuff on the same page, but they were simply too buggy for now.

Yup, no worries.

#### Johan Commelin (Jun 04 2020 at 15:49):

I think the switches are more user friendly (when they work correctly). But separate pages is developer friendly, and that's also worth something :rofl:

#### Patrick Massot (Jun 04 2020 at 15:54):

Yesterday I also modified Ryan's python code at https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/make_site.py#L134 in a way that would probably make it easier to fix the bugs. In defense of Ryan's code, I need to say that he worked on a badly specified issue. It wasn't clear in the beginning what kind of structure we wanted to support. The idea that we want exactly three levels (topic, subtopic, item) emerged while working on the list. This is now fully enforced in the YaML file (unless I missed something) and this should make everything easier (including CSS styling).

#### Patrick Massot (Jun 05 2020 at 21:45):

Another call to contributions: now that the list is visible on the website, it would be nice to write the little piece of CI that checks that urls don't break (and are correct to start with). One needs to be careful since having a successful http request is not enough to guarantee that the anchor is there: requesting https://leanprover-community.github.io/mathlib_docs/topology/basic.html#poincare_conjecture will not give you any http error.

Last updated: May 16 2021 at 22:14 UTC