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.
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
[Merged by Bors] - feat(number_theory/modular_forms/congruence_subgroups): Add definition of congruence subgroups. #15159
Conversation
…n of congruence subgroups and basic examples.
@@ -209,6 +209,29 @@ subtype.ext $ (@ring_hom.map_matrix n _ _ _ _ _ _ (int.cast_ring_hom R)).map_neg | |||
|
|||
end has_neg | |||
|
|||
section special_cases | |||
|
|||
lemma SL2_inv_det_expl (A : SL(2,R)) : det ![![A.1 1 1, -A.1 0 1], ![-A.1 1 0 , A.1 0 0]] = 1 := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't understand the name...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ok so I think what I meant to call this is SL2_inv_expl_det
for the det of the explicit inverse. But its not a great name, I'm happy to change it to something else. I guess maybe the SL
isn't needed...
…community/mathlib into congruence_subgroups
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it's ready to go, after taking into account the remaining (cosmetic) comments.
done! |
Thanks! bors merge |
…n of congruence subgroups. (#15159) This contains the definition of a congruence subgroup of `SL(2,Z)` and defines Gamma1, Gamma0 and full level subgroups. It also contains some basic results about them.
Pull request successfully merged into master. Build succeeded: |
…n of congruence subgroups. (#15159) This contains the definition of a congruence subgroup of `SL(2,Z)` and defines Gamma1, Gamma0 and full level subgroups. It also contains some basic results about them.
…n of congruence subgroups. (#15159) This contains the definition of a congruence subgroup of `SL(2,Z)` and defines Gamma1, Gamma0 and full level subgroups. It also contains some basic results about them.
This contains the definition of a congruence subgroup of
SL(2,Z)
and defines Gamma1, Gamma0 and full level subgroups. It also contains some basic results about them.