Skip to content

Bump mathlib to v4.28.0#131

Merged
kbuzzard merged 1 commit intokbuzzard:mainfrom
YaelDillies:bump_v4.28
Mar 20, 2026
Merged

Bump mathlib to v4.28.0#131
kbuzzard merged 1 commit intokbuzzard:mainfrom
YaelDillies:bump_v4.28

Conversation

@YaelDillies
Copy link
Contributor

@YaelDillies YaelDillies commented Mar 12, 2026

@erdOne, could you fix the error in Cohomology.SplittingModule? It comes from a proof you authored. or maybe @Whysoserioushah or @Paul-Lez ?

Please merge #129 first.

@Whysoserioushah
Copy link
Contributor

I fixed it but I don't have write access to your PR

@Whysoserioushah
Copy link
Contributor

The fix is to replace the two apply (config := ..) ... lines into

refine @IsIso.of_isIso_comp_right _ _ _ _ _ _ e₂.hom _ <|
    @IsIso.of_isIso_comp_left _ _ _ _ _ e₁.inv _ _ ?_

@YaelDillies
Copy link
Contributor Author

Whoops sorry, have added you now: https://github.com/YaelDillies/ClassFieldTheory/invitations

@kbuzzard kbuzzard merged commit ee1468f into kbuzzard:main Mar 20, 2026
2 checks passed
@YaelDillies YaelDillies deleted the bump_v4.28 branch March 20, 2026 14:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants