Pull request title and description conventions #

We are using the following convention for writing pull request titles and descriptions.

Format #

Note: "Title:" and "Description:" do not actually appear

  Title:
  <type>(<optional-scope>): <subject>

  Description:
  <body>
  <NEWLINE>
  <footer>
  <NEWLINE>
  <dependencies>

<type> is:

<optional-scope> is a name of module or a directory which contains changed modules. This is not necessary to include, but may be useful if the <subject> is insufficient. The Mathlib directory prefix is always omitted. For instance, it could be

<subject> has the following constraints:

<body> has the following constraints:

<footer> is optional and may contain two items:

<dependencies> if this PR depends on others, they should be listed in checkbox format, i.e., - [ ] depends on: #XXXX

Examples #

An example where <scope> is not necessary might be:

feat: have library search use the whole range for replacement

previously `apply? using h` would replace to `refine blah using h` rather than `refine blah`.

This also changes the diagnostic message to be on the whole syntax `apply? using h` rather than just the `apply?` bit, which seems fine to me.

And an example where including <scope> does add value:

docs(CategoryTheory/EssentialImage): typo and punctuation

Fix a typo, add two periods.

An example with dependent PRs:

feat: The norm on `Unitization` is a C⋆-norm

This shows that C⋆-algebras are always `RegularNormedAlgebra`s, so that their `Unitization` is equipped with a norm. Moreover, we show this norm is a C⋆-norm.

---

- [ ] depends on: #5330
- [ ] depends on: #5741
- [ ] depends on: #5742
- [ ] depends on: #5743
```