Labels

Add if increase in strong technical debt has been checked

Please do not add manually. Requests for a bot to merge automatically once CI is done.

Reply -awaiting-author to remove the label on your PR once you have addressed all comments.

This PR needs to be benchmarked before merging

This PR does not pass CI yet. This label is automatically removed once it does.

This PR was on the bors queue but came off after a build failure or other issue.

There is a Zulip discussion; the author should await and report/implement the decision reached there

This PR depends on a PR to Batteries

This PR depends on a PR to Core/Std

Not relevant for the current Lean release candidate, but will be needed for the next.

Automatically managed. Bypass by adding allow-increases-technical-debt

This PR depends on another PR (this label is automatically managed by a bot)

This PR depends on a PR to Quote4

This PR is currently being built by bors on the staging branch.

Part of the ongoing formalization of the Brownian motion and stochastic integrals

Something is not working

part of the ongoing formalization of Carleson's theorem

Part of the ongoing formalisation of class field theory

Modifies the continuous integration setup or other automation

Inactive PR (unclear if adoption would be valuable)

This pull request has been delegated to the PR author (or occasionally another non-maintainer).

Pull requests that update a dependency file

This PR bumps the version of an upstream dependency (but not toolchain).

Improvements or additions to documentation

Upstreamed from the library of formalized control theory

< 20s of review time. See the lifecycle page for guidelines.

New feature or request

A Lean module was (re)moved without a `deprecated_module` annotation

part of the ongoing formalization of Fermat's Last Theorem

Pull requests that update GitHub Actions code