Commit 2026-04-06 13:17 29f21b66

feat(NumberTheory/Modular): strengthen 2nd Fundamental-Domain Lemma (#36736) Strengthen the results on the fundamental domain for the modular group, by proving that the interior of the fundamental domain is disjoint from any translate of the fundamental domain. Proof closely follows Serre A Course in Arithmetic (although Serre also proves that S, T generate the modular group at the same time, which we do not do, since this is proved by a different method in FixedDetMatrices).