Theorem UpperHalfPlane.coe'_apply_complex

Modification history

2024-02-15 22:29

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

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

Deleted UpperHalfPlane.coe'_apply_complex View on Github →

2023-08-14 12:56

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

fix: replace SMul.smul use in UpperHalfPlane (#6353)

Added UpperHalfPlane.coe'_apply_complex View on Github →