Forward-porting #18543?

Stream: mathlib4

[Jeremy Tan]

!4#2530 says it's waiting on a forward port of mathlib3#18543, but the mathlib3 PR says "This backports a change that was already made in mathlib4."

So has mathlib3#18543 already "turned into a PR on the mathlib4 side" according to the plan on !4#2530?

[Eric Wieser]

(note that there is no mathlib3 linkifier)

[Jireh Loreaux]

(So #18543 works)