Theorem ModularGroup.coe_inj

Modification history

2025-05-12 23:33
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
refactor(Analysis/Complex/UpperHalfPlane): split off Moebius action (#24824) …
Modified ModularGroup.coe_injView on Github →
2025-05-10 12:26
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
feat(NumberTheory/ModularForms): GL2+ action is mdifferentiable (#24573) …
Added ModularGroup.coe_injView on Github →