mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Proves that the (product) sum of a list mapped through a function of the form `if x = a then ... else ...` is equal to the (product) sum over...
Informally we show `(R⧸I) ⊗ M = M/IM`. --- - [ ] depends on: #13119 If someone can golf away this dependency I'd be happy! The existing proof that `Submodule.map...
Implementation of the Berlekamp-Welch Decoding procedure, and proof of its correctness within the decoding radius. Todos: - [ ] Integrate with coding theory part of library - [ ] Gaussian...
The TupleRight section of Data.Fin.Tuple.Basic defines several operations on tuples from the right. This PR redefines these in terms of their from the left counterparts using a new `reverse` function...
Transport of exact sequences & the behavior under quotienting. --- Noting that this has merge conflicts with PR #13098. I guess whichever is merged second will have to deal with...
Lean cannot handle `CovariantClass` and `ContravariantClass` correctly - TC slowness - [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/TC.20slowness) - https://github.com/leanprover-community/mathlib4/issues/6646#issuecomment-1691792488 - It may also have made #6326 fail. - Needs a weird hack to find instance:...
Add the definition of regular sequences and induction principles for them. --- Despite the branch name this PR does not define depth. I would appreciate any suggestions on how to...
- Move definition and some lemmas from `MeasureSpaceDef` to `OuterMeasure.AE`. - Rename `MeasureTheory.Measure.ae` to `MeasureTheory.ae`. - Generalize the definition and theorems to `[OuterMeasureClass _ _]`. See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.22Almost.20every.22.20on.20outer.20measures and https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Order.20on.20measures/near/425729507...
Add some lemmas about `IsSMulRegular`. --- I'm not sure if it's okay to add the `Mathlib.GroupTheory.GroupAction.Hom` import. My understanding is that this file is kept low in the hierarchy for...
--- - [ ] depends on: #13082 I tried to limit the scope as much as possible here; there's more in https://github.com/leanprover-community/mathlib4/compare/Nat-LinearOrder-2 and https://github.com/leanprover-community/mathlib4/compare/List.Basic-no-algebra [](https://gitpod.io/from-referrer/)
