mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
--- [](https://gitpod.io/from-referrer/)
The classes `BoundedSub` and `BoundedMul` were added in PRs #12559 and #12790 to generalize subtraction and multiplication operations on bounded continuous functions (especially for the case of codomain `NNReal`). The...
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/cc.20tactic.20comes.20to.20Lean4 --- - [x] depends on: #11960 [](https://gitpod.io/from-referrer/)
Move the basic content of `GroupTheory.GroupAction` to new folders `Algebra.Group.Action` and `Algebra.GroupWithZero.Action` depending on whether it is additivisable or not. --- - [x] depends on: #12974 - [x] depends on:...
Testing some aggressive instance caching. --- [](https://gitpod.io/from-referrer/)
--- Split out from #12937 (suggestions there applied here) [](https://gitpod.io/from-referrer/)
feat: add a version of `Ideal.associatesEquivIsPrincipal` for generators that are non-zero-divisors
This PR defines the following equiv: ```lean def Ideal.associatesNonZeroDivisorsEquivIsPrincipal : Associates R⁰ ≃ {I : (Ideal R)⁰ // IsPrincipal (I : Ideal R)} ``` Also, move the definition `Ideal.associatesEquivIsPrincipal` from...
Prove that `{0, ..., k - 1} ⊆ ℤ/(n + 1)ℤ` and `{0, ..., k - 1} ⊆ ℕ` are `m`-Freiman isomorphic if `m * k ≤ n` --- -...
--- - [ ] depends on: #12268 - [ ] depends on: #12780 [](https://gitpod.io/from-referrer/)
This is consistent with the `Group` file, and drops the dependency on `Mathlib.Order` entirely. --- - [x] depends on: #13008 - [x] depends on: #13033 [](https://gitpod.io/from-referrer/)
