Typo in TopCat docstring

Stream: mathlib4

[Walter Moreira]

In Topology/Category/TopCat/Basic.lean, the docstring for TopCat seems to be incorrect:

/-- The category of semirings. -/
structure TopCat where
  ...

Is it OK to PR a fix tagged with the easy label?

[Kyle Miller]

Please make a PR!

If you can make a docstring change that takes less than 20s of review time, it can be "easy". I suppose "The category of topological spaces" is very easy to review, so it's appropriate. It's not necessary to add "easy"; often I think it's best to let the reviewers decide if it's easy or not. (So: if you're sure reviewers would agree, go ahead and mark it "easy".)

[Walter Moreira]

Thank you! Here's the PR #23075.