Proved QHat.rat_meet_zHat and QHat.rat_join_zHat.

[DjangoPeeters]

Proved QHat.rat_meet_zHat and QHat.rat_join_zHat.

[Ruben-VandeVelde]

This is great, but since you asked for feedback, here's some things I might change. Please don't let the wall of text demotivate you; I'm just hoping you might find my suggestions interesting.

[Ruben-VandeVelde]

And please also add \leanok after \begin{proof} for both lemmas in blueprint/src/chapter/ch05automorphicformexample.tex

[DjangoPeeters]

Done.

[DjangoPeeters]

Ruben, I think your 2nd lemma gave an error...

[kbuzzard]

Thanks a lot for your work on this! Can you resolve the issues which have been dealt with so I can see what's going on? Sorry, I've been dealing with real life for most of this week but now I've got more time for FLT.

[DjangoPeeters]

I'll first check if the lean and mathlib versions are compatible.

[DjangoPeeters]

Seems like my local lean version is v4.12.0 and this repo is using v4.13.0-rc3.

[DjangoPeeters]

Hmm, something about failed to synthesize RingHomClass blah. I think it is not converting the algebra morphism to a ring homomorphism in the proof of lemma _root_.Algebra.TensorProduct.one_tmul_intCast. Idk how I need to solve that right now, but I'll try using @.

[DjangoPeeters]

Due to the mathlib bump, FunLike was split and I think I need AlgHom.funLike but due to a signature change it's gonna take me some more time fixing this...

[DjangoPeeters]

It seems I have fixed it.

[pitmonticone]

Just resolved a small merge conflict.

[kbuzzard]

It seems I have fixed it.

There are many unresolved conversations. Can you resolve those which are now dealt with? Then it will be easier to see what's going on.

[kbuzzard]

I'm sorry I'm such a git amateur but this PR is currently editing a system file which it shouldn't be touching. Is someone e.g. @DjangoPeeters able to undo the random deletions which they have committed to lake-manifest.json? This is the only thing stopping this PR from being merged.

Alternatively someone can explain to me whether it's possible for me to fix this. It can't be merged because it's sabotaging a system file, but it's a PR from a fork so I don't know how to fix it.

[kbuzzard]

OK I propose merging this PR into my local master, fixing the problem and then just pushing. I don't know what github will think of this but at least it will mean that we get the results into the repo.

[kbuzzard]

these commits are now on main (other than the one editing the system file). Thanks for your contribution!