Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Merged
merged 4 commits into from
Nov 23, 2024
Merged

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

merged 4 commits into from
Nov 23, 2024

Conversation

javierlcontreras
Copy link
Contributor

@javierlcontreras javierlcontreras commented Nov 11, 2024 •
edited by github-actions bot
Loading

Code dictated by Yaël

Closes #204

kbuzzard
kbuzzard reviewed Nov 11, 2024
View reviewed changes
Copy link
Collaborator

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One of the sorries is false right now, as far as I can see.

FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Outdated Show resolved Hide resolved
FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Outdated Show resolved Hide resolved
FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean Outdated Show resolved Hide resolved
@kbuzzard
Copy link
Collaborator

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

@YaelDillies YaelDillies mentioned this pull request Nov 12, 2024
Closed
@YaelDillies
Copy link
Contributor

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
Copy link
Collaborator

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

@YaelDillies
Copy link
Contributor

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

@kbuzzard
Copy link
Collaborator

kbuzzard commented Nov 13, 2024 •
edited
Loading

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
Copy link
Contributor

This PR depends on the following mathlib PRs:

@YaelDillies YaelDillies force-pushed the TCC_11Nov_ContinuityMap branch from 0c8d1e1 to a907e0f Compare November 17, 2024 11:24
@YaelDillies
Copy link
Contributor

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

@YaelDillies YaelDillies force-pushed the TCC_11Nov_ContinuityMap branch from a907e0f to 9dd3300 Compare November 18, 2024 09:58
@YaelDillies YaelDillies force-pushed the TCC_11Nov_ContinuityMap branch from da97d09 to 1dda44d Compare November 18, 2024 12:44
@kbuzzard
Copy link
Collaborator

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

@kbuzzard kbuzzard merged commit 86c8a72 into ImperialCollegeLondon:main Nov 23, 2024
1 check passed
@YaelDillies YaelDillies deleted the TCC_11Nov_ContinuityMap branch November 23, 2024 22:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kbuzzard kbuzzard kbuzzard left review comments

@YaelDillies YaelDillies YaelDillies left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Continuity of map of local fields K_v -> L_w coming from number fields
3 participants
@javierlcontreras @kbuzzard @YaelDillies