mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
In this PR, it is shown that if `W : MorphismProperty C` has a left calculus of fractions and `C` is preadditive, then the localized category is also preadditive. ---...
We introduce lemmas on fractions which shall be useful when construction the preadditive structure on the localized category. --- - [ ] depends on: #11721 [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
Generalize 4 lemmas from `Finsupp` to `Function`. --- I don't use new lemmas to golf proofs in `Finsupp` to avoid merge conflicts with another PR I'm working on. [
Also drop a no longer needed `[DecidableEq _]` argument in 1 lemma. It was needed to generate a computable `Fintype (Set.range _)` instance but a `Finite` instance doesn't need it....
--- - [x] depends on: #10237 - [x] depends on: #10249 - [x] depends on: #10250 - [x] depends on: #10251 - [x] depends on: #10253 - [x] depends on:...
Using a `@[csimp]` attribute we can replace `npowRec` at runtime with an algorithm that uses repeated squaring, without affecting the definitional properties of `npowRec`. The prototypical application is that ```...
This PR adds lemmas showing that sets constructed by applying basic set operations to small sets are themselves small. We now have corresponding `Small ↥s` versions of almost all of...
Some results are - The ring Krull dimension and the topological dimension of the prime spectrum of a ring are the same - A field is zero-dimensional and a PID...
## Modules * `TensorProduct.finsuppLeft`, the tensor product of `ι →₀ M` and `N` is linearly equivalent to `ι →₀ M ⊗[R] N` * `TensorProduct.finsuppScalarLeft`, the tensor product of `ι →₀...
