mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Let `G` be a complete nonarchimedean abelian group and let `f : α → G` be a function. We prove that `f` is unconditionally summable if and only if `f...
Add `@[simp]` theorem `negOnePow_two_mul_add_one` to `Algebra.GroupPower.NegOnePow`, which states that `(2 * n + 1).negOnePow = -1`. Add theorems to `Algebra.Periodic` about the value of `f (x + n • c)`,...
- Move all material about Coxeter groups from GroupTheory/SpecificGroups to GroupTheory/Coxeter. - Slightly change the definition of a Coxeter system so the associated matrix actually needs to be a Coxeter...
The group of Artur Szafarczyk, Suraj Krishna M S, JB Stiegler, Isabelle Dubois, Tomáš Jakl, Lorenzo Zanichelli, Alina Yan, Emilie Uthaiwat, and I worked on a project of formalizing the...
feat: the homological functor on the homotopy category of cochain complexes in an abelian category
The homology functors on the homotopy category of cochain complexes in an abelian category are homological functors (in the sense that they send distinguished triangles to exact sequences). This PR...
This PR contains a redefinition of homology, theorems about localization of categories, including triangulated categories, a construction of the derived category of an abelian category, derived functors, spectral sequences, etc....
--- - [ ] depends on: #11740 [](https://gitpod.io/from-referrer/)
Work in progress... --- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
* `add_pow_add_pred_mem_of_pow_mem` says that (a + b) ^ (m + n - 1) belongs to an ideal I if a ^ m and b ^ n belong to that ideal...
