upper_half_plane): use `coe` instead of `coe_fn` (#12532)

Commit

3 years ago

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`.

Author

eric-wieser

Parents

c4a34136

mathlib 0d6fb8a7 - chore(analysis/complex/upper_half_plane): use `coe` instead of `coe_fn` (#12532)

mathlib
0d6fb8a7 - chore(analysis/complex/upper_half_plane): use `coe` instead of `coe_fn` (#12532)