mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Add some properties conneccting the $X$-adic valuation of a Laurent series to the vanishing of its coefficients, together with explicit values of the valuation of some basic Laurent series. Co-authored-by:...
In this WIP PR, we shall adapt the definitions in #13956, #13639 #13926 to the preadditive case. --- - [ ] depends on: #14436 - [ ] depends on: #14153...
This PR uses Arzela-Ascoli to prove local compactness of the Pontryagin dual. --- - [x] depends on: #11334 - [x] depends on: #6844 - [x] depends on: #12002 [
The contrapositive (?) of the lemma ``` theorem mem_singleton_iff {a b : α} : a ∈ ({b} : Set α) ↔ a = b := Iff.rfl ``` was missing. This...
--- The theorem is named `Walk.two_lt_chromaticNumber_of_odd_closed`, but I'm not sure if that is the best name. I didn't use the word cycle because in `Connectivity.lean` a cycle is defined as...
feat(Combinatorics/SimpleGraph): vertices are not reachable iff set of walks between them is empty
This lemma came up while extending `SimpleGraph.dist` to `ENat`. Co-authored-by: Kyle Miller --- [](https://gitpod.io/from-referrer/)
This linter emits a warning at the end of a file if there are unclosed `namespace`s or `section`s. Unlike #14352, this PR does leaves outermost `noncomputable section`s open. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linting.20for.20unclosed.20sections.3F)...
... is the product of the sublattices generated by the sets. From LeanCamCombi --- [](https://gitpod.io/from-referrer/)
This was a longstanding TODO. Kudos to Kevin for putting the pieces together! --- [](https://gitpod.io/from-referrer/)
The [Shapley-Folkman lemma](https://eml.berkeley.edu/~anderson/Econ201B/NonconvexHandout.pdf) is a convex analysis result standard in the economics literature. In contrast, it is basically unheard of in mathematics. The proof is elementary, and very similar to...