mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Prove that a bounded, a.e. continuous function on R^n is integrable on a box. In principle, this generalizes integrable_of_continuousOn, though it currently requires a.e. continuity on all of R^n rather...
This PR has basic identities satisfied by general binomial coefficients, together with corresponding lemmas about evaluating Pochhammer polynomials. --- - [ ] depends on: #13428 - [ ] depends on:...
This tactic solves problems in intuitionistic propositional logic. It also produces nice proofs when doing so, so it is useful even for proving classical theorems (using the `itauto!` variant to...
Let the group $G$ be the union of finitely many, let us say $n$, left cosets of subgroups $C₁$, $C₂$, ..., $Cₙ$: $$G = ⋃_{i = 1}^n C_i g_i.$$ Then...
... which state that if - `R` is a ring (not necessarily commutative) and `M` is a Noetherian `R`-module (based on the proof in ), or - `R` is a...
I spotted an `outParam` in an instance argument of a class. The purpose of `outParam` is to fill in the value during type class search. However, since this is an...
--- - [x] depends on: #10814 [](https://gitpod.io/from-referrer/)
Main results: + Every `normEDS` is an elliptic divisibility sequence (EDS). The key proof is `rel₄_of_anti_oddRec_evenRec`, based on my original argument first published on [MathSE](https://math.stackexchange.com/a/4903422/12932) + Conversely, every EDS is...
--- - [x] depends on: #13015 - [x] depends on: #13018 - [ ] depends on: #13019 [](https://gitpod.io/from-referrer/)
We prove that the completion of a nonarchimedean multiplicative group is a nonarchimedean multiplicative group. --- - [x] depends on: #12669 - [ ] depends on: #11837 [](https://gitpod.io/from-referrer/)
