mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Let R be a Dedekind domain with field of fractions K. This PR does two things: 1) makes the finite adeles of K/R into a K-algebra 2) turns `finiteAdeleRing` into...
In additive combinatorics, a pretty standard tool called Chang's lemma uses a version of linear independence and linear span with "scalars" restricted to `{-1, 0, 1}`. This PR defines those...
Add version of `ker_liftQ_eq_bot` with both-ways `≤` replaced by `=` in the hypotheses. --- Because of proof irrelevance, the `le_of_eq h` in the goal doesn't really matter. It'll unify with...
Equivalence between the quotient by a binary sum of submodules and an iterated quotient. --- This is a very useful "rewrite rule" when doing algebra, especially if you're doing some...
These instances make it possible to argue with multiplication and inequalities in `ℤₘ₀` . --- [](https://gitpod.io/from-referrer/) These instances are in a bit of a funny place (they need...
Move the material about `Invertible` to files under `Algebra.Group`, `Algebra.GroupWithZero`, `Algebra.Ring`. --- [](https://gitpod.io/from-referrer/)
Move its lemmas (mostly) to two new files: * `Algebra.Order.Group.Basic` for the lemmas about group-like objects * `Algebra.Order.Ring.Basic` for the lemmas about ring-like objects --- - [ ] depends on:...
Introduces the category `ContAction V G` for any concrete category `V` with a forgetful functor to `TopCat` and monoid `G`. It is realized as a full subcategory of `Action V...
In this category, we shall show that if `C` is a monoidal category and `W` is a class of morphism that is preserved by the tensor product, then the localized...
Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests. --- Mentored by @digama0; thanks for all your help. Written at...
