Notation for AbsolutelyContinuous

Stream: mathlib4

[Rémy Degenne]

Absolute continuity of measures was previously using the notation μ ≪ ν in the infoview. Now it is written μ.AbsolutelyContinuous ν instead. I guess that this is due to the recent change adding dot notation for everything. Is there a way to make the infoview use μ ≪ ν again?
The notation is defined like this:

@[inherit_doc MeasureTheory.Measure.AbsolutelyContinuous]
scoped[MeasureTheory] infixl:50 " ≪ " => MeasureTheory.Measure.AbsolutelyContinuous

[Jireh Loreaux]

I think @Kyle Miller already had a fix which might make it into rc2 this month.

[Kyle Miller]

Yeah, a fix will be in the next 4.8.0 release: https://github.com/leanprover/lean4/commit/10766297bd52e7ebc825d8c485fd507daf5ada78

Sorry for breaking these notations in rc1!