Theorem UpperHalfPlane.mul_smul'

Modification history

2025-05-19 12:23

Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean

feat(Analysis/UpperHalfPlane, ModularForms): extend actions from GLPos to GL (#24830) …

Modified UpperHalfPlane.mul_smul'View on Github →

2025-05-12 23:33

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

refactor(Analysis/Complex/UpperHalfPlane): split off Moebius action (#24824) …

Modified UpperHalfPlane.mul_smul'View on Github →

2023-06-27 21:00

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

feat: port Analysis.Complex.UpperHalfPlane.Basic (#4335)

Added UpperHalfPlane.mul_smul'View on Github →