[Merged by Bors] - feat(field_theory/adjoin): adjoining elements to fields

[tb65536]

Defines adjoining elements to fields

---

We've proven the primitive element theorem, but here's a first chunk about defining adjoining elements to fields.

[Vierkantor]

Thanks for the PR 🎉! I would really like to see it merged. I'm afraid there is still quite some work to be done, though.

[jcommelin]

@tb65536 @pglutz This is starting to look good! If you can address the outstanding remarks, I guess this is close to getting merged.

[bryangingechen]

Looks like the F[(α)] notation somehow broke one of the linters?

edit: ah, this was already pointed out here.

edit 2: I made a Zulip thread.

[bryangingechen]

Just a few some minor style and formatting suggestions.

[Vierkantor]

Looks like the F[(α)] notation somehow broke one of the linters?

edit: ah, this was already pointed out here.

edit 2: I made a Zulip thread.

I figured out the error. It's not an error in a linter, but it's the parser getting confused by scripts/lint_mathlib.lean:88:

  [(linter_name, linter, (nolint_file.find linter_name).foldl rb_map.erase decls)]),

Replacing [( and )] with [ ( and ) ] fixes the issue, but it seems that we will need to change the syntax for field extension to avoid similar problems in the future.

[tb65536]

Looks like the F[(α)] notation somehow broke one of the linters?
edit: ah, this was already pointed out here.
edit 2: I made a Zulip thread.

I figured out the error. It's not an error in a linter, but it's the parser getting confused by scripts/lint_mathlib.lean:88:

  [(linter_name, linter, (nolint_file.find linter_name).foldl rb_map.erase decls)]),

Replacing [( and )] with [ ( and ) ] fixes the issue, but it seems that we will need to change the syntax for field extension to avoid similar problems in the future.

Are you saying that we should change the field adjoin notation to F[ (a) ]?

[pglutz]

Looks like the F[(α)] notation somehow broke one of the linters?
edit: ah, this was already pointed out here.
edit 2: I made a Zulip thread.

I figured out the error. It's not an error in a linter, but it's the parser getting confused by scripts/lint_mathlib.lean:88:

  [(linter_name, linter, (nolint_file.find linter_name).foldl rb_map.erase decls)]),

Replacing [( and )] with [ ( and ) ] fixes the issue, but it seems that we will need to change the syntax for field extension to avoid similar problems in the future.

Are you saying that we should change the field adjoin notation to F[ (a) ]?

I kind of hate F[ (a) ] as notation. I propose that we pick one of the brackets here to replace [( )]. Perhaps we could use the flattened parentheses ⟮ ⟯ although there's some danger that people will get confused and think they are regular parentheses.

[fpvandoorn]

Yes, we should be careful combining multiple parentheses-like characters in a single token: that means that whenever those characters appear next to each other, they will never be interpreted as two parentheses-like characters anymore.
I'm much happier with the new parenthesis.

[jcommelin]

Looks good to me!

[Vierkantor]

Sorry for dropping out of the conversation. It looks good to me!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests