[Merged by Bors] - feat: port FieldTheory.Ratfunc

[adomani]

I am going to try to work on this for a bit, but it looks hard.

---

[adomani]

I am stopping for now: feel free to step in!

[Vierkantor]

Let me look at this for an hour or two...

[adomani]

@Vierkantor this is great, thanks! I am inching forward with removing errors!

[adomani]

Ok, I am making progress.

I unblocked a large chunk by removing the CommRing K, IsDomain K assumptions, when Field K was also present: I think that, while the omittable assumptions, might get omitted after parsing, but they mess up the proof, since they get entangled with the terms.

[adomani]

I am taking a break from this file.

There are still a few issues:

• liftRingHom just does not want to be proved by me;
• the inv_zero field of instance : Field (Ratfunc K) does not yield to frac_tac;
• num_div_denom is stopped;
• several norm_cast lemmas have a coe on the RHS (and two have broken proofs).

I suspect that some of these problems might be caused by the omit/include issue that I mentioned above. I will try to produce a #mwe to see if this is really an issue or whether I am mistaken.

Also, it would be good to check that the lemmas that now assume Field K really need it! My mathlib3 broke mid-port and I did not fix it, since I felt that I was on a roll with this file!

[Vierkantor]

several norm_cast lemmas have a coe on the RHS (and two have broken proofs).

It feels like coe_C and coe_X are false positives: the coe on the RHS applies the bundled homs, so morally I'd say it does not coerce from one type to another.

[adomani]

Well done, @Vierkantor!!

Is there an "autofix docstrings" script?

I also have a something to say about the choice of x as a symbol for a generic term in Ratfunc K and also defining X : Ratfunc K... 😄

[Vierkantor]

Is there an "autofix docstrings" script?

Yes! ./scripts/fix-comments.py. But I think we should first go through the naming conventions before we do this.

I also have a something to say about the choice of x as a symbol for a generic term in Ratfunc K and also defining X : Ratfunc K... smile

Yeah, some (variable) names are not optimal but let's postpone that change until the port is complete.

Should Ratfunc really be RatFunc? How do you change the name of the file, so that it is picked up by the automation?

I think we can just git mv Mathlib/FieldTheory/Ratfunc.lean Mathlib/FieldTheory/RatFunc.lean, because the file docstring includes the mathlib3 source files.

[adomani]

Also, I think that after fighting the non-existence of omit/include, the end result no longer needs the sectioning: after Reid's talk, I'll try to reduce the diff.

[adomani]

@Vierkantor, I "reverted" the section change: after the fact, Lean can figure out everything it seems. It was just confusing me in the course of the proof.

As for the naming convention, I am not too familiar with the capitalization rules: can someone else (maybe you? 👼 ) help with that?

[Vierkantor]

As for the naming convention, I am not too familiar with the capitalization rules: can someone else (maybe you? angel ) help with that?

Doing that right now!

[Vierkantor]

Done, I think this is ready for review again.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed:

• Build

[Vierkantor]

Let's try again (with @jcommelin's verbal approval)!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style