-
Notifications
You must be signed in to change notification settings - Fork 626
Insights: leanprover-community/mathlib4
Overview
-
- 0 Merged pull requests
- 167 Open pull requests
- 0 Closed issues
- 1 New issue
Could not load contribution data
Please try again later
167 Pull requests opened by 64 people
-
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 -
fix(Tactic/Algebraize): tactic is unable to see through assigned metavariables
#26736 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/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 -
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 -
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(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(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 -
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 -
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: 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(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
318 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(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(Topology): étalé space associated to a predicate on sections
#22782 commented on
Jul 9, 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 -
Development branch (1)
#26139 commented on
Jul 5, 2025 • 0 new comments -
chore: golf LinearAlgebra/ using `grind`
#26685 commented on
Jul 8, 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 -
feat(Topology/Instances): Cantor set is the set of ternary numbers without `1`s
#26096 commented on
Jul 5, 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(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(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: add new `simp` lemmas
#26175 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 -
WIP: define cusps
#26651 commented on
Jul 6, 2025 • 0 new comments -
feat(Counterexamples): Peano curve
#26185 commented on
Jul 5, 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(RingTheory): semisimple Wedderburn–Artin existence
#24192 commented on
Jul 5, 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(Data/Real): representation of reals from `[0, 1]` in positional system
#26021 commented on
Jul 5, 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(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: `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): the Rees theorem for depth
#26212 commented on
Jul 9, 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 -
refactor(SetTheory/Ordinal/Arithmetic): `Ordinal.IsLimit` → `Order.IsSuccLimit`
#26643 commented on
Jul 9, 2025 • 0 new comments -
feat(Algebra): depth of QuotSMulTop
#26216 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 -
chore: golf Data/ using `grind`
#26640 commented on
Jul 8, 2025 • 0 new comments -
feat(RingTheory/KrullDimension): Krull Dimension of quotient regular sequence
#26219 commented on
Jul 7, 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 -
(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: 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(Nat/Digits): use fuel in `Nat.digits`
#25864 commented on
Jul 5, 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(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(CategoryTheory/Limits/Sifted): characterization of sifted categories
#25735 commented on
Jul 5, 2025 • 0 new comments -
feat(RepresentationTheory/Homological/GroupHomology): long exact sequences
#25943 commented on
Jul 10, 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: `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: `RamifiedExtension` and `UnramifiedExtension` types for `InfinitePlace.Extension`s
#24882 commented on
Jul 8, 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 -
feat: define Riemannian manifolds
#25347 commented on
Jul 5, 2025 • 0 new comments