Commit 2025-11-14 17:31 8c73f9f0

doc(MathlibTest): demote repeated H1 headers to H2 (#31385) This PR demotes H1 headers beyond the first per file to H2. Having only a single H1 header per file is considered good practice when writing markdown. The mathlib documentation style guide does not explicitly state that a module docstring should only contain a single H1, but this seems to be taken for granted, since only the file header is requested to be an H1, while any other header mentioned is asked to be either H2 or H3.