Theorem UpperHalfPlane.ModularGroup.det_coe'

Modification history

2024-11-20 10:44

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

feat: bounds for modular forms of non-positive weights (#18192) …

Deleted UpperHalfPlane.ModularGroup.det_coe'View on Github →

2024-04-14 10:41

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

chore: remove autoImplicit from more files (#11798) …

Modified UpperHalfPlane.ModularGroup.det_coe'View on Github →

2024-02-15 22:29

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

refactor : add namespace `UpperHalfPlane.ModularGroup` (#7885) …

Added UpperHalfPlane.ModularGroup.det_coe'View on Github →