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

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


<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