ImperialCollegeLondon / FLT

Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Apache License 2.0
261 stars 48 forks source link

feat: Prove continuity of map K_v -> L_w #215

Closed javierlcontreras closed 2 days ago

javierlcontreras commented 2 weeks ago

Code dictated by Yaël

Closes #204

kbuzzard commented 2 weeks ago

Can one of you write a message just saying claim in #204 ?

YaelDillies commented 2 weeks ago

If you're against merging with a false sorry, then I suggest we wait a week or two for my refactor(s) to hit mathlib. It's quite inconvenient to work around.

kbuzzard commented 1 week ago

I'm definitely against merging with a false sorry! Sorry :-)

YaelDillies commented 1 week ago

Actually, this PR has a net count of 1 - 1 = 0 new false sorries ;)

kbuzzard commented 1 week ago

Yes but that doesn't stop me objecting to the addition of a new false sorry: I don't think total count is meaningful here. In fact the old false sorry (my fault -- a sign error) is removed on main already (which presumably is the cause of the conflict)

YaelDillies commented 1 week ago

This PR depends on the following mathlib PRs:

YaelDillies commented 1 week ago

Somehow when I merged master it overwrote the new version of the file without telling me. I'll revert what I spot

kbuzzard commented 2 days ago

Thanks! Sorry for the delay, I've been away all week.