mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
In the `Monoid` instances for `Function.End α`, `Equiv.Perm α`, `Monoid.End α`, `AddMonoid.End α`, `α →+* α`, replace the default `npowRec` by a custom one in terms of `Nat.iterate`. Write the...
This PR introduces a structure containing the data involved in a fully faithful functor `F`, i.e. inverse maps to `F.map`. (This was suggested by Andrew Yang.) This should also restore...
The bug fix lean4#4206 causes some change in the behaviour of `congr`, `convert` and friends. So some proofs need to be fixed, usually by providing more arguments. --- [
Also used the new simp lemmas to golf `AlgebraicGeometry/ProjectiveSpectrum/*` --- [](https://gitpod.io/from-referrer/)
Move all the declarations using the mathlib order hierarchy to a new file `Order.Fin`. There were a bunch of order embeddings in `Data.Fin.Basic`, so I kept an embedding version of...
--- [](https://gitpod.io/from-referrer/) The working branch for this project is [greedoid-defs](https://github.com/leanprover-community/mathlib4/tree/greedoid-defs). This branch does not contain all features of the working branch, and is for real contribution to Mathlib....
The `subsingleton` tactic tries to close equality goals by arguing that the underlying type is a subsingleton type. It might be via a `Subsingleton` instance (via `Subsingleton.elim`), but it also...
This file seems to frequently confuse `WithBot.some` and `Option.some`, and some of the lemmas are strange as a result. By teaching `cases` not to introduce `Option.some`, we no longer need...
define `rieszContentAux` under `Λ : C(X, ℝ) →ₗ[ℝ] ℝ) (hΛ : ∀ (f : C(X, ℝ)), 0 ≤ f → 0 ≤ Λ f)` and prove that it is a...
Adds some lemmas about the coefficient of polynomials of the form `X s ^ n`. Upstreamed from another project. --- [](https://gitpod.io/from-referrer/)
