Docs "#" in math mode errors

Stream: mathlib4

[Gareth Ma]

For Finset.card_erase_of_mem and some more, docs complain that "#" can't be used in Math mode. The corresponding source code is

/-- $\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$. -/
@[simp]
theorem card_erase_of_mem : a ∈ s → (s.erase a).card = s.card - 1 :=
  Multiset.card_erase_of_mem
#align finset.card_erase_of_mem Finset.card_erase_of_mem

This appears in a few more places (I think) so maybe the docs generator should be fixed instead of the docstring.

[Bhavik Mehta]

The \# notation does work in latex iirc, so when writing mathlib docstrings I would expect this to work in the online docs

[Alex J. Best]

It looks like the \ is gone by the time html is made, if this is a recent failure it could be due to https://github.com/leanprover/doc-gen4/commit/074c7832591f8dd39b53ea6d97fd1e2e5d0418e5

[Kevin Buzzard]

Does \\# work then? Or is this super-inconvenient to check?

[Alex J. Best]

I guess this is due to CMark turning \# into # as # is a way to start a new header level in markdown, so cmark needs some escaping mechanism for that. not sure what the right fix is.