CategoryTheory.Equivalence docstring

Stream: mathlib4

[Patrick Massot]

Do we agree that

/-- We infix the usual notation for an equivalence -/
infixr:10 " ≌ " => Equivalence

is a very suboptimal docstring? This showed up when I hovered to understand the obvious difference with

/-- Notation for an isomorphism in a category. -/
infixr:10 " ≅ " => Iso

Should we simply use inherit_doc (in both cases?)?