!#4335 Analysis.Complex.UpperHalfPlane.Basic

Stream: mathlib4

[Ruben Van de Velde]

I'm not managing to translate these at all - is there someone with notation / coercion experience who'd like to take a look?

-- mathport name: «expr↑ₘ »
local prefix:1024 "↑ₘ" => @coe _ (Matrix (Fin 2) (Fin 2) _) _

-- mathport name: «expr↑ₘ[ ]»
local notation:1024 "↑ₘ[" R "]" => @coe _ (Matrix (Fin 2) (Fin 2) R) _

-- mathport name: «exprGL( , )⁺»
local notation "GL(" n ", " R ")" "⁺" => Matrix.GLPos (Fin n) R

[Eric Wieser]

I think we already solved this problem in src4#SpecialLinearGroup which has the same notation trick

[Eric Wieser]

At least, for the first two

[Eric Wieser]

https://github.com/leanprover-community/mathlib4/blob/a6885a1a7f1c301ca3061ca678024788cf82aa54/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean#L91

[Ruben Van de Velde]

I've been copying from there, but somehow can't get it to work