mathlib
mathlib copied to clipboard
leanprover-community
Lean 3's obsolete mathematical components library: please use mathlib4
In this PR, we finish the proof of the general case of the Dedekind-Kummer theorem as stated in Neukirch, completing the work done in #15000. --- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
The contains the next set of results needed for #13500 . Note also the change of file name from pt1 since the name `circle_integral_transform` is no longer used (so the...
Remove `bilin_form_of_real_inner` and add a remark in the docstring of `sesq_form_of_inner` that for over real spaces the sesquilinear form is by definition a bilinear form. For this we generalize `is_self_adjoint_iff_bilin_form`...
The second part of #16449 This PR uses the suffix "ₚ" on some lemmas which assume positivity. Due to name conflicts, these similar lemmas have dissimilar names currently. If there...
The fourth part of #16449 There are still some useless lemmas that were simply ported from `algebra/order/monoid_lemmas`, this PR removes them. Also, some lemmas have both assumptions like `1 <...
I defined the category of modules following [this link](https://ncatlab.org/nlab/show/Mod). This may or may not be useful to define sheaf of modules. --- [](https://gitpod.io/from-referrer/)
+ Add new files *dfinsupp/ne_locus* and *dfinsupp/lex* mostly by copying the finsupp counterparts and making trivial adaptions. Use the `dfinsupp` lemmas/constructions to golf the `finsupp` counterpart, e.g. the `linear_order` on...
--- - [x] depends on: #16676 [](https://gitpod.io/from-referrer/)
This is one of the two functors involved in Gelfand duality. --- [](https://gitpod.io/from-referrer/)
Metadata
Owner
Metadata
Lean 3's obsolete mathematical components library: please use mathlib4