mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
We show that a holomorphic function which is periodic with a real period `h` is given by `f z = F (exp (2 * pi * I * z /...
As suggested in the [PR review](https://github.com/leanprover-community/mathlib4/pull/17783#pullrequestreview-2394779847) of #17783, there is a task of refactoring theorem statements in field theory using `IsConjRoot`. Currently the definition of `IsConjRoot` is later than most...
Co-authored-by : @jjaassoonn --- [](https://gitpod.io/from-referrer/)
In this PR, we construct the pseudofunctor `ModuleCat.restrictScalarsPseudofunctor : Pseudofunctor (LocallyDiscrete RingCatᵒᵖ) Cat` which sends a ring `R` to its category of modules: the contravariant functoriality is given by the...
Let `s` be a set of real places of the number field `K`. This PR defines the map `negAt s` on `mixedSpace K` that swaps the sign at all real...
A tool for library-scale analysis of unused imports. `lake exe unused module_1 module_2 ... module_n` will generate a markdown table with rows and columns indexed 1 through n, with an...
Generalize the content of `CategoryTheory/Grothendieck` to pseudofunctor and show that a strong oplax natural transformation of pseudofunctors induces a functor between the Grothendieck contsructions, and that the construction preserves composition...
--- Another option might be to simply make the type argument in `type` explicit, but since the API makes a lot of use of unbundled relations, that would just make...
These lemmas have one-line proofs, but I use them enough times in #15373 that I think it makes sense to introduce them. --- [](https://gitpod.io/from-referrer/)
--- - [x] depends on: #16731 - [x] depends on: #15777 - [ ] depends on: #16619 - [ ] depends on: #15424 [](https://gitpod.io/from-referrer/)
