algebraMap_apply

Stream: mathlib4

[Andrew Yang]

I just noticed the horrendously named docs#algebraMap_apply (guess what it is about!). Would someone be kind enough to propose a namespace that it should go in or (better!) open a quick PR fixing it?

[Junyan Xu]

It's in a section ContinuousMap so namespace ContinuousMap should be appropriate. It's originally added 4 years ago by @Kim Morrison in mathlib3#6782.

[Kevin Buzzard]

I can't even guess what it's about having looked in the docs!

Screenshot_20251123-131529.DuckDuckGo.png