mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Multiplicativity of smooth numbers via same of factored numbers. See #13115 for an alternative approach and for motivation of this PR. --- [](https://gitpod.io/from-referrer/)
Scatter the lemmas in `Data.Int.Parity` to earlier files: * `Algebra.Group.Int` * `Algebra.Ring.Int` --- - [x] depends on: #12821 - [x] depends on: #12882 [](https://gitpod.io/from-referrer/)
Move the `Ring` and `GroupWithZero` instances to a new file `Algebra.Ring.Rat`. --- [](https://gitpod.io/from-referrer/)
This PR adds a new file `RingTheory.Ideal.IsPrincipal` and moves most of the (basic) results about `Ideal.IsPrincipal` and `Ideal.span_singleton` from `Ideal.Basic` and `Ideal.Operations` to this file. (Some very basic results or...
Define the `Submonoid` of principal ideals and prove that `associatesEquivIsPrincipal : Associates R ≃ {I : Ideal R // Submodule.IsPrincipal I}` actually yields a `MulEquiv` between `Associates R` and this...
Contrary to what users would expect, this defines a global instance. This linter would have caught #13144 and #13170. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ConcreteCategory.2EinstFunLike.20became.20a.20.20global.20instance) Co-authored by: @adomani --- [](https://gitpod.io/from-referrer/)
Running ```bash lake exe mk_all --git ``` should have the same effect as running ```bash ./script/mk_all.sh ``` that is, it creates the files `Mathlib.lean`, `Mathlib/Tactic.lean`, `Archive.lean`, `Counterexamples.lean`. It does *not*...
WIP PR to generalise from forms to maps the results not covered in #9334 --- - [x] depends on: #9312 - [ ] depends on: #9334 [](https://gitpod.io/from-referrer/)
Some of the concepts in `LinearAlgebra/Matrix/SesquilinearForm` can be generalised from Sesquilinear Forms to Sesquilinear Maps with little or no impact on the rest of Mathlib. This PR makes those generalisations....
We define the rescaled Chebyshev polynomials $C_n$ and $S_n$ (also known as the Vieta–Lucas and Vieta–Fibonacci polynomials, respectively). They are related to the Chebyshev polynomials $T_n$ and $U_n$ by the...
