Theorem ModularGroup.coeHom_apply

Modification history

2026-04-29 15:47
Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean
refactor(Analysis/Complex/UpperHalfPlane): deprecate old GL2Pos stuff (#38700) …
Modified ModularGroup.coeHom_applyView on Github →
2025-05-12 23:33
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
refactor(Analysis/Complex/UpperHalfPlane): split off Moebius action (#24824) …
Modified ModularGroup.coeHom_applyView on Github →
2025-05-10 12:26
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
feat(NumberTheory/ModularForms): GL2+ action is mdifferentiable (#24573) …
Added ModularGroup.coeHom_applyView on Github →