mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
--- [](https://gitpod.io/from-referrer/)
... for finitely presented modules Written at the AIM algebraic geometry workshop Co-authored-by: David Swinarski --- [](https://gitpod.io/from-referrer/)
Add definition of faithfully flat ring maps and show basic properties. Co-authored-by: Florent Schaffhauser (github: matematiflo) Co-authored-by: Jujian Zhang (github:@jjaassoonn) Co-authored-by: Yunzhou Xie (github:@whysoserioushah) This contribution was created as part...
and show that they are equivalent to `Spec X.functionField ⟶ Y`. --- [](https://gitpod.io/from-referrer/)
From PFR --- I am not a huge fan of the names I came up with, so I would gladly take suggestions. [](https://gitpod.io/from-referrer/)
Move the definition of `algebraicClosure` into a separated file (mimicing `seperableClosure` in file FieldTheory.SeperableClosure). Add APIs for `algebraicClosure`. Most are copied api's from `separableClosure`. Show that every algebraic intermediate extension...
Define translation of a function by an element of its domain From LeanAPAP --- I don't really like this code, but it is foundational for discrete analysis and I have...
--- - [x] depends on: #16996 - [ ] depends on: #17016 - [x] depends on: #17026 - [ ] depends on: #18239 [](https://gitpod.io/from-referrer/)
The category-theoretic results can be split between `Mathlib/Algebra/Category/Grp/Injective.lean` and `Mathlib/Algebra/Category/ModuleCat/Injective.lean` instead, with no changes to downstream proofs. --- [](https://gitpod.io/from-referrer/)
We add a separate file in which the set of symbols of a FreeMonoid element is defined. This is separated so that users of the basic FreeMonoid file need not...
