mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
The main PR for the `have` vs `let` linter. The `have` vs `let` linter emits a warning on `have`s introducing a hypothesis whose Type is not `Prop`. There are three...
A "generic" syntax linter that can be configured using a function `Syntax → Array Syntax`. The expectations is that the function returns sub-syntax extracted from the input that should be...
Let `K` be a number field of signature `(r₁, r₂)`. This PR defines an action of the group of units `(𝓞 K)ˣ` of `K` on the space `ℝ^r₁ × ℂ^r₂`...
Add attribute [induction_eliminator] to `AddOpposite.rec'` `AdjoinRoot.induction_on` `Cycle.induction_on` `ENat.recTopCoe` `ENNReal.recTopCoe` `EReal.rec` `Finset.induction` `FreeAlgebra.induction` `FreeAddMagma.recOnAdd` `FreeAddMonoid.recOn` `FreeAddSemigroup.recOnAdd` `FreeCommRing.induction_on` `FreeSemigroup.recOnMul` `FreeMagma.recOnMul` `FreeMonoid.recOn` `LocalizedModule.induction_on` `Magma.AssocQuotient.induction_on` `ManyOneDegree.ind_on` `Module.Ray.ind` (and add `Orientation.ind` for `Orientation`, an abbrev...
--- (I definitely have not internalized the Lean4 naming conventions fully, so it's possible the names need tweaking.) I also think there probably is a more general version of the...
In this PR, it is shown that left/right Kan extensions of functors `F : C ⥤ H` along a functor `L : C ⥤ D` are compatible with changing the...
This PR introduces a weekly cron job that computes a "global" report on the evolution of Mathlib in the previous week. It consists of * a CI workflow with a...
Given a Grothendieck topology `J` on `C` and `F : A ⥤ B`, we define a type class `J.PreservesSheafification F`. We say that `F` preserves the sheafification if whenever a...
--- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
