169 Pull requests opened by 64 people

• feat(SimpleGraph): lemmas relating edges and darts to the support

  #26720 opened Jul 4, 2025

• feat(SimpleGraph): sub-walks of minimal length are also minimal

  #26722 opened Jul 4, 2025

• feat(AlgebraicGeometry): source-local closure of a morphism property

  #26723 opened Jul 4, 2025

• chore: golf Algebra/ using `grind`

  #26726 opened Jul 4, 2025

• feat(CategoryTheory/Enriched): category of enriched functors

  #26731 opened Jul 4, 2025

• chore(Algebra/Equiv/TransferInstance): split according to algebraic structures

  #26732 opened Jul 4, 2025

• feat(AlgebraicGeometry): The codimension of a point of a scheme is equal to the krull dimension of the stalk

  #26735 opened Jul 4, 2025

• fix(Tactic/Algebraize): tactic is unable to see through assigned metavariables

  #26736 opened Jul 4, 2025

• feat(AlgebraicToplogy/SimplexCategory): add notation for faces and degeneracies general truncated simplex categories

  #26738 opened Jul 4, 2025

• fix(Tactic/Algebraize): adapt application filter to `RingHom.toModule`

  #26740 opened Jul 4, 2025

• fix(Logic/Function/Basic): change precedence of uncurry prefix operator to max

  #26742 opened Jul 4, 2025

• WIP: product rule for Lie bracket on manifolds

  #26743 opened Jul 4, 2025

• feat(Probability): Hoeffding's lemma

  #26744 opened Jul 4, 2025

• feat(RingTheory): integral extensions of comm. rings are local homs

  #26746 opened Jul 4, 2025

• feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality of `CategoricalPullback`

  #26752 opened Jul 4, 2025

• feat(CategoryTheory/Limits/Shapes/Pullbacks/Categorical): the categorical pullback is invariant under equivalences of categories

  #26753 opened Jul 4, 2025

• feat(CategoryTheory/Topos): define elementary topos

  #26757 opened Jul 4, 2025

• feat(Geometry/Euclidean/Congurence): add triangle congruence

  #26758 opened Jul 4, 2025

• chore(Algebra/Polynomial/IsMonicOfDegree): do not import compute_degree tactic

  #26759 opened Jul 4, 2025

• refactor(`InformationTheory/Hamming`): Improvements to Hamming type.

  #26760 opened Jul 4, 2025

• feat(MeasureTheory/PiSystem): add π-λ theorem and SetLike instance

  #26765 opened Jul 4, 2025

• feat(Topology/MetricSpace/Bounded): add some results

  #26766 opened Jul 4, 2025

• feat(Analysis/InnerProductSpace/Adjoint): a normal idempotent operator is a star projection

  #26767 opened Jul 4, 2025

• feat(Combinatorics/Graph) : subgraph relations and operations on `Graph`

  #26770 opened Jul 4, 2025

• chore(Algebra/Equiv/TransferInstance): delete duplicated `Shrink` material

  #26774 opened Jul 5, 2025

• refactor: make `I` an outparam, and use forgetful inheritance in products

  #26776 opened Jul 5, 2025

• chore(Data/Set/Image): move `BooleanAlgebra` material to `Order`

  #26777 opened Jul 5, 2025

• feat: length of a path in a manifold

  #26778 opened Jul 5, 2025

• feat(LinearAlgebra/AffineSpace/Midpoint) add midpoint_vsub_midpoint_same_left

  #26779 opened Jul 5, 2025

• chore: golf Algebra/ using `exact`

  #26782 opened Jul 5, 2025

• feat(RingTheory/Flat): Add theorems relating Submodule.torsion and Module.Flat

  #26783 opened Jul 5, 2025

• chore: remove suppress_compilation

  #26784 opened Jul 5, 2025

• feat: beta distribution

  #26785 opened Jul 5, 2025

• fix(Order): fix simp lemma for with{Top/Bot}{Map/Congr}

  #26787 opened Jul 5, 2025

• feat(Order): Quotient lift for ArchimedeanClass

  #26789 opened Jul 5, 2025

• feat(Combinatorics/Enumerative/Bell.lean): define standard Bell number

  #26790 opened Jul 5, 2025

• feat(LinearAlgebra/Projection): add lemmas for linear projections

  #26792 opened Jul 5, 2025

• feat(Algebra/Group /ForwardDiff.lean): add five theorems for forward difference

  #26793 opened Jul 5, 2025

• chore: golf Algebra/ using combinations of `grind`, `exact`, `ext`, `simp` and `simp_all`

  #26795 opened Jul 5, 2025

• feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct`

  #26798 opened Jul 5, 2025

• feat(Analysis/VonNeumannAlgebra/Basic): idempotent in von Neumann algebra iff its range and kernel are invariant under commutant

  #26799 opened Jul 5, 2025

• chore: golf Algebra/ using `aesop_cat`

  #26801 opened Jul 5, 2025

• feat: second partial derivatives test

  #26803 opened Jul 6, 2025

• (WIP) feat(SetTheory): ZFSet is a model of ZFC

  #26804 opened Jul 6, 2025

• chore: add defeq test for grind rings

  #26806 opened Jul 6, 2025

• feat (Mathlib/Dynamics/BirkhoffSum/Basic): add lemma `birkhoffSum_of_invariant`

  #26810 opened Jul 6, 2025

• feat(LinearAlgebra/Projectivization): GL(V) action

  #26811 opened Jul 6, 2025

• feat(MeasureTheory): expose `m.SigmaAlgebra` and `IsSigmaAlgebra`

  #26814 opened Jul 6, 2025

• feat(Data/ENNReal): Add `sub_lt_iff_lt_left` and similar lemmas

  #26815 opened Jul 6, 2025

• feat(Topology): lemmas on interior and closure

  #26816 opened Jul 6, 2025

• feat(CategoryTheory/Monoidal/DayConvolution): `LawfulDayConvolutionMonoidalCategoryStruct` constructors

  #26820 opened Jul 6, 2025

• feat(LinearAlgebra/AffineSpace): affine combinations and spans of images

  #26822 opened Jul 6, 2025

• feat(LinearAlgebra/AffineSpace/Independent): interior lies in affine span

  #26823 opened Jul 6, 2025

• feat(CategoryTheory/Monoidal/DayConvolution): Day functors type synonym

  #26824 opened Jul 6, 2025

• feat(Analysis/Normed/ValuativeRel): helper instance for NormedField

  #26827 opened Jul 6, 2025

• chore(Topology): rename pi family from π to X

  #26828 opened Jul 6, 2025

• feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodule versions of ltAddSubgroup

  #26829 opened Jul 6, 2025

• feat(GroupTheory/SpecificGroups/Alternating/MaximalSubgroups): maximal subgroups of the alternating group

  #26831 opened Jul 7, 2025

• chore(Combinatorics/Additive/Energy): review API

  #26832 opened Jul 7, 2025

• feat(ValuativeRel): MulArchimedean (ValueGroupWithZero R) when IsRankLeOne

  #26833 opened Jul 7, 2025

• feat(Tactic): dependent rewriting ct'd

  #26835 opened Jul 7, 2025

• feature(Order/Lattice): Conditions for an equivalence relation to be a lattice congruence

  #26836 opened Jul 7, 2025

• feat: add lemmas about `List.scanr`

  #26838 opened Jul 7, 2025

• feat: implement the Cauchy-Riemann Equation

  #26839 opened Jul 7, 2025

• feat(Mathlib/Dynamics/BirkhoffSum/Average): add 3 BirkhoffAverage lemmas

  #26840 opened Jul 7, 2025

• feat(FieldTheory/IsGalois): map induced by the restriction to a subfield

  #26841 opened Jul 7, 2025

• feat(Mathlib/Dynamics/BirkhoffSum/Average): add lemma `birkhoffAverage_of_invariant`

  #26842 opened Jul 7, 2025

• feat(Tactic/Simproc): nested quantifiers in `existsAndEq`

  #26843 opened Jul 7, 2025

• feat: establish examples of harmonic functions

  #26844 opened Jul 7, 2025

• chore: rename ValuativeTopology to IsValuativeTopology

  #26845 opened Jul 7, 2025

• feat(Algebra/Order/Group/Cyclic): add genLTOne_unique

  #26846 opened Jul 7, 2025

• feat: multicoequalizers in the category of types

  #26847 opened Jul 7, 2025

• feat(Mathlib/Order/PartialSups): add `PartialSups` composition lemma

  #26848 opened Jul 7, 2025

• feat(AlgebraicGeometry): Any stalk of a locally noetherian scheme is Noetherian (and ditto for integral schemes)

  #26850 opened Jul 7, 2025

• feat(Mathlib/Algebra/Order/PartialSups): add 3 lemmas related to `partialSups`

  #26851 opened Jul 7, 2025

• feat(Mathlib/MeasureTheory/MeasurableSpace/Invariants): add `invariant_of_measurable_invariants`

  #26853 opened Jul 7, 2025

• feat(Analysis/InnerProductSpace/Adjoint): idempotent operator `T` is self-adjoint iff `(range T)ᗮ = ker T`

  #26855 opened Jul 7, 2025

• feat(Algebra): define associated graded structure for abelian group

  #26857 opened Jul 7, 2025

• feat(Algebra): Define the associated graded ring to filtered ring

  #26858 opened Jul 7, 2025

• feat(Algebra): Define associated graded algebra

  #26859 opened Jul 7, 2025

• feat(Algebra): Define associated graded module

  #26860 opened Jul 7, 2025

• feat(Algebra): define filtered add group hom

  #26861 opened Jul 7, 2025

• feat(Algebra): define filtered ring homomorphism

  #26862 opened Jul 7, 2025

• feat(Algebra): define filtered alghom

  #26863 opened Jul 7, 2025

• feat(VectorBundle/MDifferentiable): differentiability results for coordChange

  #26866 opened Jul 7, 2025

• feat(Algebra): filtered module hom

  #26867 opened Jul 7, 2025

• feat(Algebra): associated graded exact of exact and strict

  #26868 opened Jul 7, 2025

• feat(Algebra): exact of associated graded exact

  #26869 opened Jul 7, 2025

• feat: mdifferentiableOn_section_of_mem_baseSet₀

  #26870 opened Jul 7, 2025

• feat: finite sum, difference, scalar product of differentiable sections is differentiable

  #26871 opened Jul 7, 2025

• chore(RingTheory/Valuation/RankOne): modify the definition of Valuation.RankOne using its range rather than its codomain

  #26872 opened Jul 7, 2025

• feat(ValuativeRel): ValutiveRel on UniformSpace implies Valued

  #26874 opened Jul 7, 2025

• feat(Manifold/PartitionOfUnity): existence of global C^n smooth section for nontrivial bundles

  #26875 opened Jul 7, 2025

• chore(Analysis/InnerProductSpace/Projection): deprecating `subtypeL ∘ orthogonalProjection` in favor of `starProjection`

  #26877 opened Jul 7, 2025

• feat: declaration diff script in Lean

  #26878 opened Jul 7, 2025

• feat(CategoryTheory/Monoidal/DayConvolution): Internal homs for Day convolution

  #26879 opened Jul 7, 2025

• feat(Calculus/FDeriv/Partial): `hasStrictFDerivAt_uncurry_coprod` concerning partial derivatives

  #26880 opened Jul 7, 2025

• feat(Analysis/Calculus/Deriv/Star) A formula for `deriv (conj ∘ f ∘ conj)`

  #26881 opened Jul 7, 2025

• feat(Analysis): Additional `AsymptoticEquivalent` API

  #26882 opened Jul 7, 2025

• Universal cover

  #26884 opened Jul 7, 2025

• feat(Topology/ValuativeRel): ValuativeTopology 𝒪[K]

  #26885 opened Jul 8, 2025

• feat(NumberTheory/Padics/ValuativeRel): ValuativeRel ℚ_[p]

  #26886 opened Jul 8, 2025

• feat(Valued/WithZeroMulInt): generalize to any mul-archimedean Valued

  #26887 opened Jul 8, 2025

• refactor(SetTheory/Ordinal/Arithmetic): redefine subtraction

  #26889 opened Jul 8, 2025

• feat(CategoryTheory/Monoidal/DayConvolution) : more API for `DayFunctor`

  #26890 opened Jul 8, 2025

• feat(SetTheory/Cardinal/Aleph): `IsStrongLimit (preBeth x)`

  #26895 opened Jul 8, 2025

• feat(Data/Matrix): `Matrix.vecCons_inj` and lemmas for `vec1`, `vec2` and `vec3`

  #26896 opened Jul 8, 2025

• feat(CategoryTheory/Functor/KanExtension): transitivity of left Kan extensions

  #26899 opened Jul 8, 2025

• refactor(SetTheory/Ordinal/Arithmetic): redefine `Ordinal.IsNormal` as `Order.IsNormal`

  #26900 opened Jul 8, 2025

• added PolynomialDegree and its test

  #26901 opened Jul 8, 2025

• chore(Order/IsNormal): change default constructor

  #26903 opened Jul 8, 2025

• feat(gcongr): also use more general lemmas, closing extra goals with rfl

  #26907 opened Jul 8, 2025

• feat(CategoryTheory/Monoidal/DayConvolution): alternative ext principle for unitors

  #26908 opened Jul 8, 2025

• feat(LinearAlgebra/Projectivization/Subspace): correspondence between linear and projective subspaces

  #26909 opened Jul 8, 2025

• chore: fix naming of `mono` and `monotone`

  #26911 opened Jul 8, 2025

• chore(Algebra/Ring/Subring): simp tag `Subring.smul_def`

  #26912 opened Jul 8, 2025

• feat(NumberTheory/{*}): add a few lemmas about number field and cyclotomic extensions

  #26913 opened Jul 8, 2025

• feat(Data/PFunctor/Univariate): more definitions for univariate `PFunctor`

  #26914 opened Jul 9, 2025

• doc(Data/Int/Bitwise): add missing negation in docstring for ldiff

  #26915 opened Jul 9, 2025

• feat: product of tychonoff spaces is tychonoff

  #26917 opened Jul 9, 2025

• feat(Tactic.CategoryTheory): add associator inserting tactic

  #26920 opened Jul 9, 2025

• feat: add mdifferentiable analogues of C^n metric lemmas

  #26921 opened Jul 9, 2025

• feat: add mdifferentiable version of hom bundle smoothness lemmas

  #26922 opened Jul 9, 2025

• feat(Mathlib/Dynamics/BirkhoffSum): add the pointwise ergodic theorem (Birkhoff's)

  #26923 opened Jul 9, 2025

• chore: replace some use of `aesop` with `grind` in Algebra/

  #26924 opened Jul 9, 2025

• draft: `commandStart` more

  #26926 opened Jul 9, 2025

• feat(Topology/Order/Basic): lower set in well-order is open

  #26928 opened Jul 9, 2025

• chore: remove 3 (of 21) direct imports of `Aesop` by using `grind`

  #26929 opened Jul 9, 2025

• feat(CategoryTheory/Enriched): `V`-enriched isomorphisms

  #26931 opened Jul 9, 2025

• feat(SkewMonoidAlgebra): multiplication and algebraic instances

  #26933 opened Jul 9, 2025

• feat(RingTheory/DedekindDomain/Ideal): add HeightOneSpectrum.ofPrime

  #26934 opened Jul 9, 2025

• feat(Analysis/SpecialFunction/NthRoot): definition and basic API of Real.nthRoot

  #26935 opened Jul 9, 2025

• feat(RingTheory/DividedPowes/SubDPIdeal): complete lattice and quotients

  #26936 opened Jul 9, 2025

• chore: `n+1` to `n + 1`

  #26937 opened Jul 9, 2025

• chore(gcongr): set `synthAssignedInstances := false`

  #26938 opened Jul 9, 2025

• feat(Algebra/Order/Monoid): StrictMono.isOrdered(Cancel)Monoid

  #26939 opened Jul 9, 2025

• chore(GroupWithZero/WithZero): use `recZeroCoe` for `WithZero.lift'`

  #26941 opened Jul 9, 2025

• feat(RingTheory/Valuation/ValueGroupIso): isomorphism of value groups when compatible

  #26942 opened Jul 9, 2025

• chore(Valuation/Archimedean): generalize `isPrincipalIdealRing_iff_not_denselyOrdered` to only discuss mrange

  #26943 opened Jul 9, 2025

• chore: remove 6 (of 26) direct imports of `Mathlib.Tactic.Abel` by using `grind`

  #26944 opened Jul 9, 2025

• feat(LinearAlgebra/AffineSpace/AffineSubspace): basic properties of `sInf` and `iInf`

  #26945 opened Jul 9, 2025

• feat(Algebra): two lemmas about IsScalarTower and SMulCommClass on commutative monoids

  #26948 opened Jul 9, 2025

• chore: remove 4 (of 7) direct imports of `Mathlib.Tactic.Tauto` by using `grind`

  #26949 opened Jul 9, 2025

• Primitives of holomorphic functions and path integral

  #26950 opened Jul 9, 2025

• chore: remove 11 (of 37) direct imports of `Mathlib.Tactic.Ring` by using `grind`

  #26951 opened Jul 9, 2025

• feat(CategoryTheory/DayConvolution): monoid objects internal to day convolutions

  #26952 opened Jul 9, 2025

• chore: use `edist` instead of `dist` in `TendstoInMeasure`

  #26954 opened Jul 10, 2025

• feat(LinearAlgebra/OnSup): extend linear maps to sums of modules

  #26955 opened Jul 10, 2025

• feat(RingTheory/DividedPowers/Basic): add divided power structure on pZp

  #26956 opened Jul 10, 2025

• feat(Algebra): unmixed thm of Cohen-Macaulay ring

  #26957 opened Jul 10, 2025

• feat(AlgebraicTopology): path objects in model categories

  #26958 opened Jul 10, 2025

• feat(AlgebraicTopology/ModelCategory): the lemma by K. S. Brown

  #26960 opened Jul 10, 2025

• feat(RingTheory/PowerSeries/Substitution): add API

  #26961 opened Jul 10, 2025

• feat(Data/Nat/Fib/Basic): some API for `Nat.fib`

  #26962 opened Jul 10, 2025

• chore: remove whitespace

  #26963 opened Jul 10, 2025

• chore: a batch of whitespace fixes

  #26964 opened Jul 10, 2025

• feat: add root system induction principle equivalent to connectedness of Dynkin diagram

  #26965 opened Jul 10, 2025

• feat: the Dedekind-MacNeille completion

  #26966 opened Jul 10, 2025

• feat(AlgebraicTopology/ModelCategory): left homotopies

  #26967 opened Jul 10, 2025

• feat(Order/Concept): sets in a concept are codisjoint

  #26968 opened Jul 10, 2025

• feat(CategoryTheory): localization of quotient categories

  #26972 opened Jul 10, 2025

• feat(Geometry/Diffeology): diffeologies generated from sets of plots

  #26973 opened Jul 10, 2025

• feat: a norm_num extension for complex numbers

  #26975 opened Jul 10, 2025

• refactor(Order/Concept): rename `intentClosure` → `lowerPolar`

  #26976 opened Jul 10, 2025

• chore: remove 3 (of 12) direct imports of `Mathlib.Tactic.NormNum` by using `grind`

  #26977 opened Jul 10, 2025

• feat: induction principle for open sets according to a basis

  #26978 opened Jul 10, 2025

• feat(Topology/GDelta/Basic): add lemmas about unions of meagre sets

  #26979 opened Jul 10, 2025

• feat(Algebra/GroupWithZero/WithZero): add lemma map'_surjective_iff

  #26980 opened Jul 10, 2025

• chore: golf using `grw`

  #26981 opened Jul 10, 2025

1 Issue opened by 1 person

• Tracking Issue: Digraph Targets

  #26771 opened Jul 5, 2025

321 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem

  #26660 commented on Jul 7, 2025 • 50 new comments

• feat: add `BooleanSigmaAlgebra`

  #26318 commented on Jul 10, 2025 • 36 new comments

• feat(AlgebraicTopology): cylinder objects in model categories

  #26171 commented on Jul 10, 2025 • 21 new comments

• feat(Control/Monad/Free): define free monad, prove it lawful, and implement standard effects

  #25491 commented on Jul 6, 2025 • 12 new comments

• feat(Combinatorics/Enumerative/Stirling.lean): define Stirling numbers of the first and second kind

  #26290 commented on Jul 7, 2025 • 11 new comments

• feat(NumberTheory/Divisors): add int divisors

  #26158 commented on Jul 7, 2025 • 11 new comments

• feat(SetTheory/ZFC): Define the language of sets and state the ZFC axioms

  #26644 commented on Jul 8, 2025 • 10 new comments

• feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range

  #26588 commented on Jul 10, 2025 • 10 new comments

• feat(SetTheory/ZFC/Ordinal): Lean ordinals to ZFC ordinals

  #26544 commented on Jul 10, 2025 • 9 new comments

• feat(NumberTheory/Padics): the completion of `ℚ` at a finite place is `ℚ_[p]`

  #21950 commented on Jul 8, 2025 • 7 new comments

• feat(CategoryTheory/Localization): the right derivability structure given by functorial resolutions

  #26029 commented on Jul 7, 2025 • 7 new comments

• feat(Geometry/Euclidean/Congurence): add triangle congruence

  #25175 commented on Jul 9, 2025 • 7 new comments

• feat(RingTheory/Presentation): core of a presentation

  #24794 commented on Jul 4, 2025 • 6 new comments

• feat(AlgebraicGeometry): Add global preorder instance for schemes

  #26204 commented on Jul 9, 2025 • 6 new comments

• feat(SimpleGraph): sub-walks

  #26655 commented on Jul 7, 2025 • 6 new comments

• feat: random variables are independent iff their joint distribution is the product measure

  #26265 commented on Jul 4, 2025 • 5 new comments

• feat: restricted power series form a ring

  #26089 commented on Jul 7, 2025 • 5 new comments

• refactor(Probability/ProbabilityMassFunction): Make constructions use NNReal

  #26596 commented on Jul 7, 2025 • 4 new comments

• feat(RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum

  #26368 commented on Jul 11, 2025 • 4 new comments

• feat: projections and injections for WithLp

  #26498 commented on Jul 4, 2025 • 4 new comments

• feat(Topology): étalé space associated to a predicate on sections

  #22782 commented on Jul 9, 2025 • 4 new comments

• feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space

  #26300 commented on Jul 8, 2025 • 4 new comments

• feat(SimpleGraph): add more API for `take`/`drop`

  #26614 commented on Jul 7, 2025 • 4 new comments

• feat(Bicategory/CatEnriched): 2-cat from Cat-enriched cat

  #25784 commented on Jul 8, 2025 • 3 new comments

• feat(SetTheory/Cardinal/Aleph): characterization of initial successor ordinals

  #26607 commented on Jul 6, 2025 • 3 new comments

• feat(LinearAlgebra/Projection): lemmas on projections and invariant submodules

  #25874 commented on Jul 11, 2025 • 3 new comments

• feat(Data/Sum/Order): `toLex` as a `RelIso`

  #26617 commented on Jul 7, 2025 • 3 new comments

• feat(RingTheory): lemmas on finiteness of `LinearMap` and `Module.End`

  #24015 commented on Jul 8, 2025 • 2 new comments

• feat(Tactic/Order): support `⊤`, `⊥`, and lattice operations

  #26354 commented on Jul 9, 2025 • 2 new comments

• feat: equivalent condition for subgroups to be simple

  #26552 commented on Jul 11, 2025 • 2 new comments

• add `Fin.cycleIcc` which rotates `range(i, j)` and refactor `cycleRange`

  #26195 commented on Jul 9, 2025 • 2 new comments

• feat(CategoryTheory/Monoidal/Opposite): the equivalence `Cᴹᵒᵖᴹᵒᵖ ≌ C` is monoidal

  #25767 commented on Jul 10, 2025 • 2 new comments

• feat: IMO 2001 Q4

  #25786 commented on Jul 8, 2025 • 2 new comments

• feat(RepresentationTheory/Homological/GroupHomology): add Shapiro's lemma

  #25996 commented on Jul 10, 2025 • 2 new comments

• feat(Combinatorics/SimpleGraph): Add Subgraph.inclusion_edge_apply_coe and inclusion_edgeSet_apply_coe

  #25248 commented on Jul 9, 2025 • 1 new comment

• feat(LinearAlgebra/Contraction): bijectivity of `dualTensorHom` + generalize to CommSemiring

  #25284 commented on Jul 6, 2025 • 1 new comment

• feat(RingTheory): faithfully flat ring maps

  #24530 commented on Jul 5, 2025 • 1 new comment

• chore(RingTheory): add `Algebra (FractionRing R) (FractionRing S)`

  #25611 commented on Jul 7, 2025 • 1 new comment

• feat(FieldTheory): abelian extensions

  #23669 commented on Jul 9, 2025 • 1 new comment

• Feat(CategoryTheory): terminal categories with an application to hoFunctor

  #25781 commented on Jul 5, 2025 • 1 new comment

• feat(CategoryTheory): transport symmetric monoidal structure along equivalence

  #25796 commented on Jul 10, 2025 • 1 new comment

• feat: add Mathlib.RingTheory.DedekindDomain.Instances

  #26070 commented on Jul 6, 2025 • 1 new comment

• feat(SetTheory/Cardinal/Aleph): `o.card ≤ ℵ_ o` and variants

  #26608 commented on Jul 6, 2025 • 1 new comment

• feat(RingTheory/Valuation/Discrete/Basic): add uniformizer API

  #26591 commented on Jul 10, 2025 • 1 new comment

• feat(RingTheory/PolynomialLaw/Basic): extends polynomial laws to arbitrary universes

  #26719 commented on Jul 7, 2025 • 1 new comment

• feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation

  #26160 commented on Jul 5, 2025 • 0 new comments

• WIP: tactic analysis for calls to `linarith` that can become `grind`

  #26683 commented on Jul 8, 2025 • 0 new comments

• feat(Topology): continuous surjection from Cantor set to Hilbert cube

  #26149 commented on Jul 5, 2025 • 0 new comments

• chore(GeomSum): split into ring vs field and non-ordered vs ordered parts

  #26142 commented on Jul 5, 2025 • 0 new comments

• chore: golf LinearAlgebra/ using `grind`

  #26685 commented on Jul 8, 2025 • 0 new comments

• Development branch (1)

  #26139 commented on Jul 5, 2025 • 0 new comments

• Development branch (2)

  #26138 commented on Jul 7, 2025 • 0 new comments

• feat(Topology/Instances): Cantor set is homeomorphic to `ℕ → Bool`

  #26136 commented on Jul 5, 2025 • 0 new comments

• feat: sharp monoids

  #26110 commented on Jul 5, 2025 • 0 new comments

• feat(NumberField/IsCM): first results about the action of `complexConjugation` on units

  #26107 commented on Jul 6, 2025 • 0 new comments

• feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers

  #26101 commented on Jul 10, 2025 • 0 new comments

• chore: golf Combinatorics/ using `grind`

  #26689 commented on Jul 7, 2025 • 0 new comments

• chore: golf CategoryTheory/ using `grind`

  #26691 commented on Jul 7, 2025 • 0 new comments

• chore: golf Computability/ using `grind`

  #26693 commented on Jul 7, 2025 • 0 new comments

• feat(RepresentationTheory/Homological/GroupHomology): long exact sequences

  #25943 commented on Jul 10, 2025 • 0 new comments

• feat(MeasureTheory.VectorMeasure): add lemma which shows that variation of a `ℝ≥0∞` VectorMeasure is equal to itself

  #26165 commented on Jul 5, 2025 • 0 new comments

• feat(MeasureTheory.VectorMeasure) : variation defined as a supremum is equal to variation defined using the Hahn-Jordan decomposition.

  #26168 commented on Jul 5, 2025 • 0 new comments

• feat(AlgebraicTopology/ModelCategory): a trick by Joyal

  #26169 commented on Jul 6, 2025 • 0 new comments

• feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): 2-functoriality of `CatCommSqOver`

  #26679 commented on Jul 5, 2025 • 0 new comments

• feat: add new `simp` lemmas

  #26175 commented on Jul 5, 2025 • 0 new comments

• feat(RingTheory/Finiteness/Defs): span of a set is finitely generated iff generated by a finite subset

  #26653 commented on Jul 5, 2025 • 0 new comments

• feat(CategoryTheory/Limits): Fubini for products

  #26178 commented on Jul 5, 2025 • 0 new comments

• feat(Topology): every compact metric space is image of Cantor set

  #26184 commented on Jul 5, 2025 • 0 new comments

• feat(Counterexamples): Peano curve

  #26185 commented on Jul 5, 2025 • 0 new comments

• WIP: define cusps

  #26651 commented on Jul 6, 2025 • 0 new comments

• chore(TensorProduct): remove more `suppress_compilation`s

  #26648 commented on Jul 6, 2025 • 0 new comments

• feat: subcomplexes of a classical CW complex

  #26201 commented on Jul 9, 2025 • 0 new comments

• feat(Data/Sym/Sym2): lift commutative operations to sym2

  #26647 commented on Jul 7, 2025 • 0 new comments

• feat(Algebra): associated primes of localized module

  #26210 commented on Jul 8, 2025 • 0 new comments

• feat(Algebra): vanishing of induced hom between ext

  #26211 commented on Jul 9, 2025 • 0 new comments

• feat(Algebra): the Rees theorem for depth

  #26212 commented on Jul 9, 2025 • 0 new comments

• feat: the empty line in commands linter

  #25945 commented on Jul 8, 2025 • 0 new comments

• feat(Analysis/InnerProductSpace/MulOpposite): defines the inner product on opposite spaces

  #25951 commented on Jul 11, 2025 • 0 new comments

• feat(RepresentationTheory/Homological/GroupHomology/Functoriality): the degree 1 part of the corestriction-coinflation exact sequence when the subgroup acts trivially

  #25952 commented on Jul 10, 2025 • 0 new comments

• refactor: Abstract out the substructure lattice construction and SetLike closure operators

  #25963 commented on Jul 5, 2025 • 0 new comments

• feat(RepresentationTheory/Homological/GroupHomology/Functoriality): the degree 1 part of the corestriction-coinflation exact sequence

  #25969 commented on Jul 10, 2025 • 0 new comments

• feat(RingTheory): decompose archimedean classes of HahnSeries

  #25970 commented on Jul 6, 2025 • 0 new comments

• refactor(AlgebraicGeometry/EllipticCurve/*): replace Fin 3 with products

  #25988 commented on Jul 5, 2025 • 0 new comments

• feat(AlgebraicGeometry/EllipticCurve): generalise nonsingular condition

  #25991 commented on Jul 5, 2025 • 0 new comments

• feat(Topology/Compactification): projective line over ℝ is homeomorphic to the one-point compactification of ℝ

  #25999 commented on Jul 10, 2025 • 0 new comments

• feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree

  #26000 commented on Jul 4, 2025 • 0 new comments

• feat(CategoryTheory/Monoidal/Action): action of `Type` on categories with coproducts

  #26002 commented on Jul 5, 2025 • 0 new comments

• feat(`Algebra/Group/Prod`): Add API for inclusion and projection maps from and to the product of units.

  #26010 commented on Jul 5, 2025 • 0 new comments

• feat: add elementary lifts for `OneHom`, `MulHom`, `MonoidHom` and `RingHom`.

  #26011 commented on Jul 5, 2025 • 0 new comments

• feat: Low-level derivatives of lifts on `OneHom`, `MulHom` and `MonoidHom`

  #26012 commented on Jul 5, 2025 • 0 new comments

• feat: Add high-level generalizations from `MonoidHom` lifts

  #26015 commented on Jul 5, 2025 • 0 new comments

• feat(Analysis/NormedSpace/FunctionSeries): Add SummableUniformlyOn ve…

  #26016 commented on Jul 7, 2025 • 0 new comments

• feat(RingTheory/TensorProduct/FG) : direct limit properties of tensor products wrt finitely generated submodules

  #26717 commented on Jul 7, 2025 • 0 new comments

• feat(Data/Real): representation of reals from `[0, 1]` in positional system

  #26021 commented on Jul 5, 2025 • 0 new comments

• feat(RingTheory/MvPolynomial/Groebner): add docstring and a particular case

  #26022 commented on Jul 10, 2025 • 0 new comments

• chore: golf Algebra/ using `aesop`

  #26704 commented on Jul 7, 2025 • 0 new comments

• feat(Analysis/Polynomial/MahlerMeasure): the Mahler measure of a complex polynomial

  #26035 commented on Jul 8, 2025 • 0 new comments

• feat(Order): bicartesian squares in lattices

  #26037 commented on Jul 4, 2025 • 0 new comments

• feat: `mon_tauto`, a simp set to prove tautologies about a monoid object

  #26057 commented on Jul 5, 2025 • 0 new comments

• feat(Topology/StoneCech): exists_continuous_surjection_from_StoneCech_to_dense_range

  #26067 commented on Jul 8, 2025 • 0 new comments

• chore: golf AlgebraicTopology/ using `grind`

  #26699 commented on Jul 7, 2025 • 0 new comments

• feat: Add `id` and `comp` classes for `FunLike` and `refl`, `trans` and `symm` classes for `EquivLike`

  #26071 commented on Jul 5, 2025 • 0 new comments

• feat(NumberField/CMField): A totally complex abelian extension of ℚ is CM

  #26073 commented on Jul 7, 2025 • 0 new comments

• chore: golf RingTheory/ using `grind`

  #26698 commented on Jul 7, 2025 • 0 new comments

• chore: golf Geometry/ using `grind`

  #26697 commented on Jul 9, 2025 • 0 new comments

• chore: make `finiteness` a default tactic

  #26090 commented on Jul 5, 2025 • 0 new comments

• feat(Topology/Instances): Cantor set is the set of ternary numbers without `1`s

  #26096 commented on Jul 5, 2025 • 0 new comments

• feat: `Real.sin_eq_one_iff` and similar

  #26383 commented on Jul 5, 2025 • 0 new comments

• feat(RingTheory/Perfectoid): Fontaine's theta map is surjective

  #26384 commented on Jul 5, 2025 • 0 new comments

• feat(RingTheory/Perfectoid): define integral perfectoid rings

  #26385 commented on Jul 5, 2025 • 0 new comments

• Update Orthogonal.lean

  #26597 commented on Jul 4, 2025 • 0 new comments

• feat(RingTheory/Perfectoid): Fontaine's theta map and the de Rham period rings

  #26388 commented on Jul 5, 2025 • 0 new comments

• feat: $C^1$ vector fields on compact manifolds define global flows

  #26395 commented on Jul 5, 2025 • 0 new comments

• refactor(ModelTheory): tidy up proof of Ax-Grothendieck with definable functions

  #26399 commented on Jul 5, 2025 • 0 new comments

• feat(Analysis/ODE/MaximalSolution): Existence of maximal solutions for ODE meeting Picard-Lindelöf conditions

  #26413 commented on Jul 5, 2025 • 0 new comments

• feat(Mathlib/Data/Nat/Prime/Defs): fuel Nat.minFac

  #26436 commented on Jul 5, 2025 • 0 new comments

• refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure

  #26446 commented on Jul 7, 2025 • 0 new comments

• feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): bicategory-like lemmas for `CatCospanTransforms`

  #26447 commented on Jul 5, 2025 • 0 new comments

• refactor: simplify `(f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)` to `(f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂)`

  #26448 commented on Jul 4, 2025 • 0 new comments

• feat(NumberTheory/LocalFields/Basic): provide the definition of (valued) Local Field

  #26449 commented on Jul 7, 2025 • 0 new comments

• WIP - feat (LinearAlgebra/RootSystem): API for CartanMatrix

  #26455 commented on Jul 9, 2025 • 0 new comments

• feat(Mathlib/GroupTheory/Perm/MaximalSubgroups): maximal subgroups of the permutation group

  #26457 commented on Jul 10, 2025 • 0 new comments

• feat(LinearAlgebra): generators of pi tensor products

  #26464 commented on Jul 7, 2025 • 0 new comments

• feat(Algebra/Module): presentation of the `PiTensorProduct`

  #26465 commented on Jul 5, 2025 • 0 new comments

• feat(AlgebraicTopology/SimplexCategory/Augmented): the canonical monoid object in the augmented simplex category

  #26466 commented on Jul 5, 2025 • 0 new comments

• feat(LinearAlgebra): the tensor product of a finite family of free modules is free

  #26467 commented on Jul 5, 2025 • 0 new comments

• feat(NumberTheory): `N(I 𝓞L) = N(I) ^ [L:K]` for an integral ideal `I` of `K`

  #26474 commented on Jul 10, 2025 • 0 new comments

• feat(Geometry/Diffeology): basics of diffeological spaces

  #26484 commented on Jul 10, 2025 • 0 new comments

• feat(Mathlib/Algebra/GroupWithZero/Range): add withZeroUnitsHom

  #26589 commented on Jul 8, 2025 • 0 new comments

• feat: Alexandrov discrete implies locally path-connected

  #26492 commented on Jul 10, 2025 • 0 new comments

• feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): equivalences of categorical cospans

  #26579 commented on Jul 5, 2025 • 0 new comments

• feat(RingTheory/Valuation/IntegrallyClosed): the valuation subring is integrally closed

  #26526 commented on Jul 7, 2025 • 0 new comments

• feat(Geometry/Euclidean/Incenter): signs of barycentric coordinates of touchpoints

  #26530 commented on Jul 7, 2025 • 0 new comments

• feat(CategoryTheory/Limits/Pullbacks/Categorical/CatCospanTransform): adjunctions of categorical cospans

  #26578 commented on Jul 5, 2025 • 0 new comments

• feat(CategoryTheory/Limits/Shapes/Pullback/Categorical/CatCospanTransform): more lemmas about isomorphisms of `CatCospanTransform`

  #26547 commented on Jul 6, 2025 • 0 new comments

• feat(Valued/LocallyCompact): locally compact iff complete and DVR and finite residue field

  #26549 commented on Jul 7, 2025 • 0 new comments

• feat(LiminfLimsup): liminf of an antitone function is its supremum

  #26561 commented on Jul 6, 2025 • 0 new comments

• feat(CategoryTheory/Topos): subobject classifier without limits

  #26556 commented on Jul 10, 2025 • 0 new comments

• feat(Algebra): Ext iso quotient regular sequence

  #26213 commented on Jul 9, 2025 • 0 new comments

• feat(Algebra): definition of depth

  #26214 commented on Jul 9, 2025 • 0 new comments

• feat(Algebra): Auslander-Buchsbaum theorem

  #26215 commented on Jul 9, 2025 • 0 new comments

• feat(Algebra): depth of QuotSMulTop

  #26216 commented on Jul 9, 2025 • 0 new comments

• refactor(SetTheory/Ordinal/Arithmetic): `Ordinal.IsLimit` → `Order.IsSuccLimit`

  #26643 commented on Jul 9, 2025 • 0 new comments

• feat(Algebra): Ischebeck theorem

  #26217 commented on Jul 9, 2025 • 0 new comments

• feat(Algebra): definition of cohen macaulay

  #26218 commented on Jul 10, 2025 • 0 new comments

• feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence

  #26219 commented on Jul 7, 2025 • 0 new comments

• chore: golf Data/ using `grind`

  #26640 commented on Jul 8, 2025 • 0 new comments

• Mr. Covariant Derivatives

  #26221 commented on Jul 10, 2025 • 0 new comments

• chore: adaptation for leanprover/lean4#8884

  #26227 commented on Jul 5, 2025 • 0 new comments

• chore(Combinatorics/SimpleGraph/Walk): split SimpleGraph.Path

  #26234 commented on Jul 5, 2025 • 0 new comments

• chore: add deprecations for split of SimpleGraph.Path

  #26241 commented on Jul 5, 2025 • 0 new comments

• feat(Algebra): cohen macaulay local ring is catenary

  #26245 commented on Jul 10, 2025 • 0 new comments

• chore(Units): better follow the naming convention

  #26251 commented on Jul 5, 2025 • 0 new comments

• chore: golf Analysis/ using `grind`

  #26639 commented on Jul 8, 2025 • 0 new comments

• feat(Analysis/Calculus): Taylor series converges to function on whole ball

  #26267 commented on Jul 4, 2025 • 0 new comments

• (benchmark) for lean4#9147

  #26628 commented on Jul 5, 2025 • 0 new comments

• chore(Analysis/Analytic): split `Analytic.Basic`

  #26270 commented on Jul 10, 2025 • 0 new comments

• feat(AlgebraicGeometry): Simple lemma about existence of affine neighbourhoods

  #26271 commented on Jul 7, 2025 • 0 new comments

• feat: a theorem of Jordan on primitive subgroups of the permutation group

  #26282 commented on Jul 10, 2025 • 0 new comments

• fix: make `CompleteLattice` extend `BoundedOrder`

  #26626 commented on Jul 5, 2025 • 0 new comments

• feat: filtering lists and bounded quantifiers are primitive recursive

  #26295 commented on Jul 9, 2025 • 0 new comments

• perf: the `commandStart` linter only acts on modified files

  #26299 commented on Jul 8, 2025 • 0 new comments

• chore: update Mathlib dependencies 2025-07-02

  #26625 commented on Jul 5, 2025 • 0 new comments

• feat(AlgebraicTopology): the fundamental lemma of homotopical algebra

  #26303 commented on Jul 5, 2025 • 0 new comments

• feat(RingTheory/Valuation/Discrete/Basic): relate DVRs and discrete valuations

  #26623 commented on Jul 10, 2025 • 0 new comments

• "Junk value" test file

  #26330 commented on Jul 10, 2025 • 0 new comments

• feat(Algebra/Polynomial): Descartes' Rule of signs

  #26331 commented on Jul 10, 2025 • 0 new comments

• refactor(SetTheory/Ordinal/FixedPoint): redefine `Ordinal.deriv`

  #26603 commented on Jul 8, 2025 • 0 new comments

• feat(CategoryTheory): make `Functor.comp` irreducible

  #26601 commented on Jul 5, 2025 • 0 new comments

• feat(RingTheory): semisimple Wedderburn–Artin existence

  #24192 commented on Jul 5, 2025 • 0 new comments

• feat: add `Fin.cycleIcc` which rotates `range(i, j)`

  #24139 commented on Jul 8, 2025 • 0 new comments

• feat(Topology/UniformSpace/OfCompactT2): generalize theorem

  #24103 commented on Jul 9, 2025 • 0 new comments

• feat(Topology): Completely Regular Space iff Uniformizable

  #24096 commented on Jul 11, 2025 • 0 new comments

• feat (Types.Colimits): Quot is functorial and colimitEquivQuot is natural

  #23990 commented on Jul 9, 2025 • 0 new comments

• feat: SkewPolynomial

  #23949 commented on Jul 9, 2025 • 0 new comments

• feat(Topology): cardinality of connected components is bounded by cardinality of fiber

  #23835 commented on Jul 5, 2025 • 0 new comments

• feat(Linter.openClassical): also lint for Classical declarations as …

  #23763 commented on Jul 5, 2025 • 0 new comments

• feat(Combinatorics/SimpleGraph): every circuit contains a cycle proof

  #23637 commented on Jul 5, 2025 • 0 new comments

• refactor: merge `DomMulAct` and `DomAddAct` into `DomAct`

  #23594 commented on Jul 8, 2025 • 0 new comments

• chore(RingTheory/AdicCompletion/AsTensorProduct): golf using five lemma for modules

  #23497 commented on Jul 5, 2025 • 0 new comments

• refactor(Topology/UniformSpace): use `Rel`

  #23181 commented on Jul 11, 2025 • 0 new comments

• feat: more lemmas about ordered groups with zero

  #23177 commented on Jul 9, 2025 • 0 new comments

• feat(MetricSpace): nets

  #23124 commented on Jul 6, 2025 • 0 new comments

• feat(RingTheory/Congruence/Hom): copy from GroupTheory

  #22954 commented on Jul 5, 2025 • 0 new comments

• refactor: reimplement `RingQuot` in terms of `RingCon.Quotient`

  #22952 commented on Jul 5, 2025 • 0 new comments

• feat(CategoryTheory): infrastructure for inclusion morphisms into products in categories with 0-morphisms

  #22928 commented on Jul 5, 2025 • 0 new comments

• feat(RingTheory/TensorProduct/DirectLimit/FG): direct limit of finitely generated submodules and tensor product

  #22898 commented on Jul 5, 2025 • 0 new comments

• chore: fix `Scheme.Hom.appTop`

  #22820 commented on Jul 5, 2025 • 0 new comments

• feat: `RamifiedExtension` and `UnramifiedExtension` types for `InfinitePlace.Extension`s

  #24882 commented on Jul 8, 2025 • 0 new comments

• feat: injectivity of `InfinitePlace.embedding`

  #24875 commented on Jul 6, 2025 • 0 new comments

• refactor: add `hom` lemmas for the `MonoidalCategory` structure on `ModuleCat`

  #24823 commented on Jul 5, 2025 • 0 new comments

• feat(RingTheory): group-like elements

  #24730 commented on Jul 7, 2025 • 0 new comments

• feat(LinearAlgebra/Matrix/NonsingularInverse): inverting `Matrix` inverts its `LinearEquiv`

  #24719 commented on Jul 6, 2025 • 0 new comments

• chore(Data/Set): `tsum` version of `Set.encard_iUnion_of_finite` for non-finite types

  #24710 commented on Jul 5, 2025 • 0 new comments

• feat(Topology/Algebra/Valued): `IsLinearTopology 𝒪[K] K` and `𝒪[K] 𝒪[K]`

  #24627 commented on Jul 6, 2025 • 0 new comments

• chore: rename field `inf` to `min` in `Lattice`

  #24614 commented on Jul 5, 2025 • 0 new comments

• chore: make `Valuation.Completion` a `def` and refactor more of `AdicValuation.lean`

  #24590 commented on Jul 8, 2025 • 0 new comments

• test

  #24558 commented on Jul 5, 2025 • 0 new comments

• test

  #24489 commented on Jul 5, 2025 • 0 new comments

• chore(RingTheory/Valuation/Discrete/Basic): add ordered Iso between Z_{m0} and the value group

  #24435 commented on Jul 7, 2025 • 0 new comments

• feat(CategoryTheory): descent of morphisms for a pseudofunctor

  #24411 commented on Jul 5, 2025 • 0 new comments

• refactor(Topology/Algebra/Module/WeakDual): Clean up

  #24405 commented on Jul 6, 2025 • 0 new comments

• feat: distributive Haar characters of `ℝ` and `ℂ`

  #24383 commented on Jul 5, 2025 • 0 new comments

• feat(Algebra/AlgHom): `Unique` if target is `Subsingleton`

  #24379 commented on Jul 5, 2025 • 0 new comments

• feat: fderiv lemmas for `pow`

  #24351 commented on Jul 5, 2025 • 0 new comments

• feat(FieldTheory): fg extension over perfect field is separably generated

  #24350 commented on Jul 5, 2025 • 0 new comments

• chore: replace `WithLp.equiv` with a new pair `WithLp.toLp`/`WithLp.ofLp`

  #24261 commented on Jul 5, 2025 • 0 new comments

• feat(CategoryTheory/Sites): Equivalence of categories of sheaves with a dense subsite that is 1-hypercover dense

  #19444 commented on Jul 5, 2025 • 0 new comments

• feat: universal properties of vector bundle constructions

  #17627 commented on Jul 5, 2025 • 0 new comments

• refactor(Algebra/Group): make `IsUnit` a typeclass

  #17458 commented on Jul 5, 2025 • 0 new comments

• feat(ModelTheory/Equivalence): The quotient type of formulas modulo a theory

  #16801 commented on Jul 5, 2025 • 0 new comments

• feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFunOfBivariate

  #16743 commented on Jul 8, 2025 • 0 new comments

• feat(CI): check for badly formatted titles or missing/contradictory labels

  #16303 commented on Jul 5, 2025 • 0 new comments

• feat: combinatorial maps and planar graphs

  #16074 commented on Jul 5, 2025 • 0 new comments

• dev: add Mathlib.Tactic.Linter.ForallIntro

  #15213 commented on Jul 5, 2025 • 0 new comments

• feat(Algebra/ModuleCat): descent data

  #14203 commented on Jul 5, 2025 • 0 new comments

• chore: replace continuity -> fun_prop in remaining directories

  #14009 commented on Jul 5, 2025 • 0 new comments

• feat(Algebra/SkewMonoidAlgebra/Basic): add SkewMonoidAlgebra

  #10541 commented on Jul 9, 2025 • 0 new comments

• draft for Van Kampen

  #10084 commented on Jul 5, 2025 • 0 new comments

• refactor: Add norm_num machinery for NNRat

  #9915 commented on Jul 7, 2025 • 0 new comments

• feat(RingTheory/GradedAlgebra/HomogeneousIdeal): generalize to homogeneous submodule

  #9820 commented on Jul 5, 2025 • 0 new comments

• feat: covering maps from properly discontinuous actions and discrete subgroups

  #7596 commented on Jul 5, 2025 • 0 new comments

• Sperner's lemma

  #25231 commented on Jul 4, 2025 • 0 new comments

• Turn `compute_degree` into a simproc

  #22219 commented on Jul 8, 2025 • 0 new comments

• Implement Lusztig / Geck's construction of semisimple Lie algebras

  #21964 commented on Jul 7, 2025 • 0 new comments

• Tracking issue: Ordinal refactors

  #17033 commented on Jul 8, 2025 • 0 new comments

• feat(Homotopy/Lifting): monodromy of covering maps and lifting criterion

  #22771 commented on Jul 5, 2025 • 0 new comments

• refactor: make use of `FunLike` for `Submonoid.LocalizationMap`

  #22655 commented on Jul 5, 2025 • 0 new comments

• chore: deduce `Nat.multiplicity` lemmas from the `Nat.factorization` ones

  #22503 commented on Jul 5, 2025 • 0 new comments

• feat(CategoryTheory/Abelian): Noetherian objects form a Serre class

  #22367 commented on Jul 5, 2025 • 0 new comments

• feat(RingTheory/DividedPowers/RatAlgebra): add definitions

  #22322 commented on Jul 9, 2025 • 0 new comments

• feat: weak approximation theorems for infinite places of a number field

  #22153 commented on Jul 8, 2025 • 0 new comments

• feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg

  #22151 commented on Jul 5, 2025 • 0 new comments

• feat: collections of distinct infinite places contain values that diverge around 1

  #22147 commented on Jul 8, 2025 • 0 new comments

• feat: collections of non-trivial and pairwise inequivalent absolute values contain values that diverge around 1

  #22142 commented on Jul 8, 2025 • 0 new comments

• feat: two inequivalent absolute values have a `< 1` and `> 1` value

  #22100 commented on Jul 8, 2025 • 0 new comments

• feat(RingTheory/Localization/Pi): localization of a finite direct product where each semiring in product has maximal nilradical is a projection

  #22018 commented on Jul 5, 2025 • 0 new comments

• feat: extensible `push`(_neg) tactic - part 1

  #21965 commented on Jul 5, 2025 • 0 new comments

• feat: decomposition into independent atoms

  #21871 commented on Jul 10, 2025 • 0 new comments

• feat: the ring of integers of a `ℤₘ₀`-valued field is compact whenever it is a DVR and the residue field is finite

  #21844 commented on Jul 8, 2025 • 0 new comments

• fix: prevent `exact?` recursing forever on `n = 55`

  #20784 commented on Jul 5, 2025 • 0 new comments

• chore(GroupTheory/Index): rename `relindex` to `relIndex`

  #19872 commented on Jul 5, 2025 • 0 new comments

• refactor: review the `simps` projections of `OneHom`, `MulHom`, `MonoidHom`

  #19860 commented on Jul 5, 2025 • 0 new comments

• feat: L'Hopital's rule from within a convex set

  #19796 commented on Jul 5, 2025 • 0 new comments

• refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction

  #19668 commented on Jul 5, 2025 • 0 new comments

• feat(CategoryTheory/Monoidal/Action): action of opposite categories

  #25861 commented on Jul 5, 2025 • 0 new comments

• perf(Data.Real.Sqrt): make Real.sqrt irreducible

  #25856 commented on Jul 7, 2025 • 0 new comments

• feat/refactor: redefinition of homology + derived categories

  #25848 commented on Jul 8, 2025 • 0 new comments

• feat (RingTheory/HahnSeries): Powers of a binomial

  #25831 commented on Jul 9, 2025 • 0 new comments

• refactor (RingTheory/HahnSeries/HEval): remove positive order condition from definition

  #25830 commented on Jul 9, 2025 • 0 new comments

• WIP: experiments with vertex algebras

  #25822 commented on Jul 9, 2025 • 0 new comments

• chore: kill coercion from EquivLike to Equiv

  #25816 commented on Jul 5, 2025 • 0 new comments

• feat(SimpleGraph): Weaker condition for paths in acyclic graphs

  #25814 commented on Jul 4, 2025 • 0 new comments

• feat(data): List.Chain' helper lemmas

  #25812 commented on Jul 4, 2025 • 0 new comments

• feat(Condensed): closed symmetric monoidal structure on light condensed modules

  #25797 commented on Jul 5, 2025 • 0 new comments

• feat(CategoryTheory): localization preserves braided structure

  #25794 commented on Jul 5, 2025 • 0 new comments

• chore: remove >6 month old material in `Deprecated`

  #25790 commented on Jul 7, 2025 • 0 new comments

• the homotopy category functor preserves products

  #25780 commented on Jul 8, 2025 • 0 new comments

• feat(CategoryTheory/Bicategory/NaturalTransformations): strong and lax natural transformations of lax functors

  #25779 commented on Jul 5, 2025 • 0 new comments

• chore: deprime `induction` in `Analysis`

  #25776 commented on Jul 7, 2025 • 0 new comments

• feat(AlgebraicTopology/SimplicialSet/NerveAdjunction): to Strict Segal 2

  #25775 commented on Jul 5, 2025 • 0 new comments

• chore: deprime `induction` in `AlgebraicTopology/CategoryTheory`

  #25774 commented on Jul 9, 2025 • 0 new comments

• chore: fix more induction/recursor branch names

  #25770 commented on Jul 7, 2025 • 0 new comments

• feat(AlgebraicTopology/SimplexCategory/Augmented): monoidal structure on `AugmentedSimplexCategory`

  #25743 commented on Jul 5, 2025 • 0 new comments

• feat(RepresentationTheory/Homological/GroupHomology/Functoriality): low degree functoriality maps

  #25939 commented on Jul 10, 2025 • 0 new comments

• feat(Algebra/Order/Ring): make `IsOrderedRing.toStrictOrderedRing` an instance

  #25933 commented on Jul 5, 2025 • 0 new comments

• refactor(CategoryTheory): redefine triangulated subcategories using ObjectProperty

  #25931 commented on Jul 10, 2025 • 0 new comments

• WIP towards Hecke bound for q-expansions

  #25930 commented on Jul 5, 2025 • 0 new comments

• feat(RepresentationTheory/Homological/GroupHomology/LowDegree): `H₁(G, A) ≃+ Gᵃᵇ ⊗[ℤ] A` when `A` is trivial

  #25929 commented on Jul 10, 2025 • 0 new comments

• feat(gcongr): let `gcongr` take a depth parameter, analogous to `congr`

  #25928 commented on Jul 5, 2025 • 0 new comments

• feat(RingTheory/AdicCompletion): more APIs for IsAdicComplete

  #25927 commented on Jul 4, 2025 • 0 new comments

• docs: Add documentation to miscellaneous files

  #25917 commented on Jul 5, 2025 • 0 new comments

• feat: add an ext lemma for the opposite category

  #25914 commented on Jul 5, 2025 • 0 new comments

• feat(Algebra/Ring/Idempotent): subtraction lemmas for idempotents and star projections

  #25910 commented on Jul 7, 2025 • 0 new comments

• feat(RepresentationTheory/Homological/GroupHomology/LowDegree): specialized API for `H0, H1, H2`

  #25908 commented on Jul 10, 2025 • 0 new comments

• feat (Topology/Compactness/CompactSystem): Closed and compact square cylinders form a compact system.

  #25906 commented on Jul 5, 2025 • 0 new comments

• feat(Bicategory/Opposites): add 1-cell opposite bicategory

  #25901 commented on Jul 5, 2025 • 0 new comments

• feat (Topology/Compactness/CompactSystem): Set system of finite unions of sets in a compact system is again a compact system

  #25900 commented on Jul 5, 2025 • 0 new comments

• fix(Tactic/Widget/Conv): fix various issues

  #25889 commented on Jul 5, 2025 • 0 new comments

• feat(RepresentationTheory/Homological/GroupHomology/LowDegree): Identify `cycles A n` with `cyclesₙ A` for `n = 0, 1, 2`

  #25888 commented on Jul 10, 2025 • 0 new comments

• feat: add `IsSMulTorsionFree`

  #25887 commented on Jul 5, 2025 • 0 new comments

• feat(CategoryTheory/Monoidal/Action): actions as monoidal functors to endofunctors

  #25875 commented on Jul 5, 2025 • 0 new comments

• feat(Nat/Digits): use fuel in `Nat.digits`

  #25864 commented on Jul 5, 2025 • 0 new comments

• feat: define Riemannian manifolds

  #25347 commented on Jul 5, 2025 • 0 new comments

• feat: `Mon_ C` is cartesian-monoidal if `C` is

  #25326 commented on Jul 5, 2025 • 0 new comments

• feat: regular local rings

  #25283 commented on Jul 5, 2025 • 0 new comments

• refactor: make `MonoidAlgebra` into a one-field structure

  #25273 commented on Jul 5, 2025 • 0 new comments

• feat: `counit (antipode a) = counit a`

  #25267 commented on Jul 5, 2025 • 0 new comments

• Projective contraction

  #25247 commented on Jul 5, 2025 • 0 new comments

• refactor: redefine perfect pairings as a Prop-valued typeclass

  #25239 commented on Jul 10, 2025 • 0 new comments

• feat(Tactic/ComputeDegree): add support for scalar multiplication with different types

  #25238 commented on Jul 5, 2025 • 0 new comments

• feat(Algebra): Quadratic Algebra

  #25223 commented on Jul 10, 2025 • 0 new comments

• feat(AlgebraicGeometry): Tate normal form of elliptic curves

  #25218 commented on Jul 5, 2025 • 0 new comments

• feat: Finset.sum induction for tensor products.

  #25197 commented on Jul 5, 2025 • 0 new comments

• feat: `(M →* N₁) ≃* (M →* N₂)` if `N₁ ≃* N₂`

  #25182 commented on Jul 5, 2025 • 0 new comments

• feat: `#print sorries`, a command to find usage of `sorry`

  #25179 commented on Jul 4, 2025 • 0 new comments

• feat(EllipticCurve): basic API for singular cubics

  #25071 commented on Jul 5, 2025 • 0 new comments

• chore(Finsupp): move order properties under `Order`

  #25002 commented on Jul 5, 2025 • 0 new comments

• chore(Algebra/Notation): separate very basic lemmas about `Set.indicator` and `Pi.single`

  #24998 commented on Jul 6, 2025 • 0 new comments

• fix(Topology/Covering): switch to standard definition

  #24983 commented on Jul 9, 2025 • 0 new comments

• feat: affine monoids

  #24912 commented on Jul 5, 2025 • 0 new comments

• feat: `ramificationIdx` for `NumberField.InfinitePlace`

  #24884 commented on Jul 8, 2025 • 0 new comments

• feat(CategoryTheory/Limits/Sifted): characterization of sifted categories

  #25735 commented on Jul 5, 2025 • 0 new comments

• feat(CategoryTheory/Monoidal/Limits): miscellany about preservation of (co)limits by tensor products

  #25732 commented on Jul 5, 2025 • 0 new comments

• experiment: grind instead of omega

  #25729 commented on Jul 5, 2025 • 0 new comments

• (WIP) Galois group of `x ^ n - x - 1`

  #25726 commented on Jul 5, 2025 • 0 new comments

• feat: write the `field_simp` tactic

  #25697 commented on Jul 5, 2025 • 0 new comments

• refactor: generalize `OreSet` to work for bimodules

  #25671 commented on Jul 5, 2025 • 0 new comments

• chore: redefine `LocalizedModule`

  #25662 commented on Jul 5, 2025 • 0 new comments

• refactor: overhaul instances on LocalizedModule

  #25622 commented on Jul 5, 2025 • 0 new comments

• refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces

  #25578 commented on Jul 5, 2025 • 0 new comments

• feat: define `∃ x > y, ...` notation to mean `∃ x, y < x ∧ ...`

  #25573 commented on Jul 5, 2025 • 0 new comments

• feat(Category/Grpd): define the bicategory of groupoids

  #25561 commented on Jul 5, 2025 • 0 new comments

• feat(SetTheory/ZFC/Rationals): define rationals in ZFC

  #25488 commented on Jul 5, 2025 • 0 new comments

• feat(SetTheory/ZFC/Integers): define integers in ZFC

  #25486 commented on Jul 5, 2025 • 0 new comments

• feat(SetTheory/ZFC/Naturals): define natural numbers in ZFC

  #25485 commented on Jul 5, 2025 • 0 new comments

• feat(SetTheory/ZFC/Booleans): define Boolean algebra in ZFC

  #25484 commented on Jul 5, 2025 • 0 new comments

• chore(Data/Set/Prod, SetTheory/ZFC/Basic): add theorem prod_subset_of_prod and extend ZFC model

  #25483 commented on Jul 5, 2025 • 0 new comments

• test for .lean/.md check

  #25474 commented on Jul 5, 2025 • 0 new comments

• chore: remove some duplicate instances

  #25410 commented on Jul 5, 2025 • 0 new comments

• feat: `CommAlgCat` is cocartesian-monoidal

  #25365 commented on Jul 7, 2025 • 0 new comments