wrong link for Complex.abs in documentation

leanprover-community / mathlib4

The math library of Lean 4

https://leanprover-community.github.io/mathlib4_docs

Apache License 2.0

1.47k stars 321 forks source link

wrong link for Complex.abs in documentation #15415

Open PhoenixIra opened 2 months ago

PhoenixIra commented 2 months ago

It appears that Complex.abs gets wrongly linked here: Analysis/SpecialFunction/Complex/Arg (and probably also at other positions) to the general definition of abs instead of the complex one at Data/Complex/Abs.

I unfortunately do not know how to fix that.

YaelDillies commented 1 month ago

Can you upstream this issue to doc-gen4? That's where it would be solved

PhoenixIra commented 2 weeks ago

Sorry, I was busy with thesis writing and then forgot this issue. Its now upstreamed.