mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
We prove that in a nonarchimedean ring, $$\sum_{(i, j) \in I \times J} a_i b_j = \left(\sum_{i \in I} a_i \right)\left(\sum_{j \in J} b_j\right),$$ provided that both sums on the...
Let `M` be a topological space with a continuous multiplication operation and a zero. We prove that if `f : α → M` and `g : β → M` are...
Multiplicativize `Topology.Algebra.GroupCompletion`. That is, rewrite it in the multiplicative setting and recover the original results using `@[to_additive]`. - Because `@[to_additive]` doesn't work with `noncomputable section` (https://github.com/leanprover/lean4/pull/2610), some instances with `@[to_additive]`...
Prove the following. - `Inducing.hasProd_iff` / `Inducing.hasSum_iff`: Let $g \colon \beta \to \alpha$ be an inducing homomorphism of topological additive commutative monoids. A series $\sum_{i \in I} b_i$ unconditionally converges...
We prove the [equational criterion for flatness](https://stacks.math.columbia.edu/tag/00HK). As a consequence, every homomorphism from a finitely presented module to a flat module factors through a finite free module. --- - [x]...
We define the standard geometric representation of a Coxeter group and prove that it is faithful. --- - [ ] depends on: #11526 [](https://gitpod.io/from-referrer/)
This PR is a container for several smaller PRs that refactor and generalize the existing Hahn series theory. It is (I think) all we need from Hahn series to get...
--- [](https://gitpod.io/from-referrer/)
We add some theorems and instances for Hahn Modules, in particular, a `HahnSeries Γ R`-module structure on `HahnModule Γ R V` for `R` a semiring and `V` an `R`-module. Some...
This is the way following [zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311920.20towards.20proj.20construction) suggested by Jöel and Andrew. --- [](https://gitpod.io/from-referrer/)
