mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Lemma of B. H. Neumann on covering a group by finitely many cosets of subgroups. --- [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/generic.20great.20circle.20on.20the.20sphere.20misses.20any.20finite.20set/near/439361300) [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
change
--- [](https://gitpod.io/from-referrer/)
Now that the Lean frontend normalises all line endings to LF (since leanprover/lean4#3903), this check is not necessary any more. It is also one fewer Python linter to rewrite in...
This PR extends the `ring` tactic with a new config argument `char` which will try to reduce all constant terms modulo the given characteristic. This allows `ring` to prove e.g....
TODO: Name the stuff properly and finish the proofs. Suggestions on naming would be greatly appreciated.
This PR introduces a linter for suggesting bugs in tactics. See * #12077 * #12083 * #12084 for some bugs exposed by the test suite. --- [](https://gitpod.io/from-referrer/)
Add the more interesting direction of topology comparison for the Lévy-Prokhorov distance. Conclude that if the underlying space is separable, then the topology of convergence in distribution coincides with the...
`IsDedekindDomain.HeightOneSpectrum.adicCompletion` is currently a `def` and this causes a bunch of `rw`s to fail in Lean 4; `erw` is needed. In developing the API further I ran into more irritating...
--- [](https://gitpod.io/from-referrer/)