mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
This commit is generated using rg -l generalizedEigenspace | xargs sed -i 's/generalizedEigenspace/genEigenspace/g' rg -l maximalGeneralizedEigenspace | xargs sed -i 's/maximalGeneralizedEigenspace/maxGenEigenspace/g' The upshot is many shorter lemma names. --- [
The files containing lemmas about the interaction of order in terms of `CovariantClass`/`ContravariantClass` and *not* the bundled compatibility typeclasses were all over the place. This PR puts them all in...
over a field of characteristic zero, when the Killing form is non-singular --- - [ ] depends on: #13076 [](https://gitpod.io/from-referrer/)
We add `Polynomial.nmem_nonZeroDivisors_iff`, known as McCoy's theorem: a polynomial `P : R[X]` is a zerodivisor if and only if there is `a : R` such that `a ≠ 0` and...
--- [](https://gitpod.io/from-referrer/)
It is still annoyingly painful to prove that two finsets have equal size by exhibiting a bijection between. This PR remedies this problem by copying over the lemmas that show...
Add the fixed point theorem for (omega) complete partial orders and Kleene's fixed point theorem for complete lattices. --- Some comments regarding this PR: - I decided to use the...
Prove the corners theorem and Roth's theorem as corollaries of the triangle removal lemma --- - [ ] depends on: #12551 - [x] depends on: #12570 - [x] depends on:...
For `G` a commutative monoid and a set `A` in `G × G` , define corners of `A` as solutions to `x₁ + y₂ = x₂ + y₁` where `(x₁,...
