Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-09 11:28 0d6fb8a7

View on Github →

chore(analysis/complex/upper_half_plane): use coe instead of coe_fn (#12532) This matches the approach used by other files working with special_linear_group.

Estimated changes