mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
`Int.strongRec`: if a proposition holds for integers less than a threshold, and it holds for an integer above the threshold if it holds for all smaller integers, then it holds...
--- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
Additivise a few more lemmas. Unify `inv_mem_center`/`inv_mem_center₀`, `div_mem_center`/`div_mem_center₀`. Move the few remaining lemmas about `GroupWithZero` to a new file `Algebra.GroupWithZero.Center`. Do the same with `Algebra.Group.Centralizer`. --- - [x] depends on:...
The to_additive version of this lemma was incorrectly named in Lean 3, which seemingly led to some confusion in porting --- [](https://gitpod.io/from-referrer/)
--- This method can improve speed, for example #7434, #7435, #7401, #6874, #7408, #7430, #7435, #7436 Sometimes it slows things dow though, e.g #7431 [](https://gitpod.io/from-referrer/)
This adds definitions of linear equivalences for modules `M` with their left-/right-product with a trivial module `M \times 0` and `0 \times M`, and analogous statements for Algebras. --- [
Move the few remaining lemmas to earlier files. --- [](https://gitpod.io/from-referrer/)
We show that the automorphism group of a fiber functor is isomorphic to the limit of the automorphism groups of all Galois objects. From this we deduce that the automorphism...
Not everyone contributes to Mathlib by first asking for write permission: see #7339 for an example. For those users, it's nice if it is at least possible to change `awaiting-review`...
