3 Pull requests merged by 1 person

• chore: adaptations for nightly-2024-10-31

  #18487 merged Oct 31, 2024

• chore: adaptations for nightly-2024-10-30

  #18435 merged Oct 31, 2024

• chore: adaptations for nightly-2024-10-29

  #18421 merged Oct 30, 2024

154 Pull requests opened by 54 people

• chore: make tests into a library

  #18304 opened Oct 27, 2024

• Feat: projective line over ℝ is homeomorphic to the one-point compactification of ℝ

  #18306 opened Oct 27, 2024

• chore(Filter/Prod): drop `Filter.prod`, use `SProd` instead

  #18315 opened Oct 28, 2024

• feat(AlgebraicGeometry): typeclasses for `S`-schemes

  #18321 opened Oct 28, 2024

• feat(Topology/ContinuousMap/*): add some simp lemmas

  #18326 opened Oct 28, 2024

• feat(FieldTheory/AlgebraicClosure): `minpoly x F` splits in `E` implies `minpoly x F` splits in `algebraicClosure F E`

  #18331 opened Oct 28, 2024

• feat(Algebra/Module): presentation of the cokernel of a linear map

  #18332 opened Oct 28, 2024

• feat(Condensed): a sequential limit of epimorphisms in light condensed modules is epimorphic

  #18336 opened Oct 28, 2024

• feat(RingTheory/LaurentSeries): finishes the proof that LaurentSeries are the X-adic completion of Rational Functions

  #18346 opened Oct 28, 2024

• feat: add list lemmas

  #18349 opened Oct 28, 2024

• feat(AlgebraicGeometry): prime spectrum of jacobson rings are jacobson spaces

  #18353 opened Oct 28, 2024

• chore(scripts/bench): use `LEAN`, not `--lean`

  #18354 opened Oct 28, 2024

• feat(AlgebraicGeometry/Morphisms): finite morphisms

  #18357 opened Oct 28, 2024

• feat(Algebra/Module): presentation of a direct sum of modules

  #18359 opened Oct 28, 2024

• refactor(HasPDF): use structure fields

  #18371 opened Oct 29, 2024

• feat(Algebra/Module): the tautological presentation of a module

  #18374 opened Oct 29, 2024

• feat(Topology/ENNReal): Add `ENNReal.tsum_biUnion`

  #18379 opened Oct 29, 2024

• chore(RingTheory/DedekindDomain/Ideal): generalize count_associates_factors_eq

  #18388 opened Oct 29, 2024

• feat(Algebra/Module): presentation of the restriction of scalars of a module

  #18389 opened Oct 29, 2024

• feat: `μ (Prod.fst ⁻¹' {x}) = ∑' y, μ {(x, y)}`

  #18390 opened Oct 29, 2024

• feat: a `n`-torsion group is a `n`-group

  #18391 opened Oct 29, 2024

• feat: the quotient by a subgroup containing multiples of `n` is `n`-torsion

  #18395 opened Oct 29, 2024

• feat: the Lie algebra of a Lie group over R or C

  #18396 opened Oct 29, 2024

• chore: Rename `RestrictGenTopology` to `Topology.IsRestrictGen`

  #18397 opened Oct 29, 2024

• chore(Topology): miscellaneous renames

  #18398 opened Oct 29, 2024

• feat: symmetry of the second derivative over R or C

  #18399 opened Oct 29, 2024

• feat(Integral/Pi): a version of `polarCoord` for `pi` integrals

  #18400 opened Oct 29, 2024

• feat: cardinality of the graph of a function

  #18401 opened Oct 29, 2024

• feat: introduce `ContinuousLinearMap.IsInvertible` and basic API

  #18402 opened Oct 29, 2024

• feat: add Algebra.compHom and related lemma

  #18404 opened Oct 29, 2024

• refactor(LinearAlgebra/SesquilinearForm): Hermitian sesquilinear maps

  #18406 opened Oct 29, 2024

• feat: improve the Analysis.Analytic.OfScalars API and implement it for geometric and exponential functions

  #18407 opened Oct 29, 2024

• feat(FieldTheory): minimal polynomials determine an algebraic extension (Isaacs 1980)

  #18412 opened Oct 29, 2024

• feat(CategoryTheory/Enriched): functoriality of the enrichment of functor categories

  #18414 opened Oct 29, 2024

• feat: any function is integrable on a finset wrt to a finite measure

  #18415 opened Oct 29, 2024

• feat(RingTheory): the residue field of a prime ideal

  #18416 opened Oct 29, 2024

• refactor: generalize `SMul (Ideal R) (Submodule R M)` to `SMul (Submodule R A) (Submodule R M)`

  #18419 opened Oct 30, 2024

• feat(RingTheory/UFD): `WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt`

  #18422 opened Oct 30, 2024

• feat(LinearAlgebra): charpoly of base-change of linear map

  #18423 opened Oct 30, 2024

• feat(RingTheory/TensorProduct): Add `Algebra.baseChange_lmul`

  #18424 opened Oct 30, 2024

• feat(SetTheory/Ordinal/Arithmetic): `a < b + c ↔ ∃ d < c, a ≤ b + d`

  #18427 opened Oct 30, 2024

• feat(FieldTheory): new Adjoin lemmas and finish up #17543

  #18430 opened Oct 30, 2024

• feat(Algebra): misc lemmas and cleanup

  #18431 opened Oct 30, 2024

• feat(Algebra/Module): presentation of the tensor product

  #18432 opened Oct 30, 2024

• feat(RingTheory/Algebraic[Independent]): some more results on transcendental and algebraically independent

  #18433 opened Oct 30, 2024

• chore(IsAlgClosed/Classification): Make theorems more universe polymorphic

  #18434 opened Oct 30, 2024

• refactor: add refactored APIs for algebraic filter bases

  #18437 opened Oct 30, 2024

• refactor: adapt `KrullTopology` to the new algebraic filter bases API

  #18438 opened Oct 30, 2024

• refactor: use new algebraic filter bases API in `FiniteAdeleRing`

  #18439 opened Oct 30, 2024

• feat(Algebra/Module): a presentation of an algebra induces a presentation of the module of differentials

  #18440 opened Oct 30, 2024

• refactor(AdicTopology): use new API for algebraic filter bases, and factor some code

  #18441 opened Oct 30, 2024

• feat(Topology/Algebra): Krasner's lemma

  #18444 opened Oct 30, 2024

• feat(AtTopBot/Archimedean): weaken TC assumptions

  #18445 opened Oct 30, 2024

• feat(Combinatorics/SimpleGraph/Clique): add clique number

  #18446 opened Oct 30, 2024

• chore(Computability/TuringMachine): split `TuringMachine.lean`

  #18448 opened Oct 30, 2024

• chore(Filter/Bases): split

  #18450 opened Oct 30, 2024

• feat: `divRadical` for polynomials

  #18452 opened Oct 30, 2024

• feat: add dsimp lemma for SetLike

  #18453 opened Oct 30, 2024

• feat: add imp_forall_iff_forall

  #18455 opened Oct 30, 2024

• feat: add simp annotation to Subtype.val_injective

  #18457 opened Oct 30, 2024

• feat: add CompleteSublattice.subtype

  #18458 opened Oct 30, 2024

• Valuation.map_sum_eq_of_lt

  #18460 opened Oct 30, 2024

• feat: left and right common multiples mixins

  #18461 opened Oct 30, 2024

• chore(SuccPred/Limit): rename 2 lemmas

  #18462 opened Oct 30, 2024

• feat(SetTheory/Ordinal/Notation/FundamentalSequence): define type of fundamental sequences

  #18463 opened Oct 30, 2024

• perf: lower the priority of `toMul` and `toAdd` instances

  #18464 opened Oct 30, 2024

• feat(Data/List/Sort): `Sorted r l → Sorted r (filter f l)`

  #18466 opened Oct 30, 2024

• doc(SetTheory/Game/PGame): improve docstrings

  #18467 opened Oct 30, 2024

• perf: lower the priority of `Ordered*.to*` instances

  #18468 opened Oct 30, 2024

• chore(SetTheory/Game/PGame): deprecate primed lemmas

  #18469 opened Oct 30, 2024

• perf: lower the priority of `Normed*.to*` instances

  #18470 opened Oct 30, 2024

• perf: lower the priority of `Comm*.to*` instances

  #18472 opened Oct 30, 2024

• feat(Data/List/Basic): lemmas relating `find?` to `head` of `dropWhile`

  #18473 opened Oct 30, 2024

• perf: lower the priority of `*WithOne.to*` instances

  #18474 opened Oct 30, 2024

• feat(Rat/Cast/Order): add `@[gcongr]` lemmas

  #18475 opened Oct 31, 2024

• feat(Order/Basic): add `gcongr` lemmas

  #18476 opened Oct 31, 2024

• chore: use FourierTransformCLM for Poisson formula

  #18477 opened Oct 31, 2024

• feat(Order/WellFoundedOn): wfon.mapsTo and sdff_singleton

  #18480 opened Oct 31, 2024

• feat(GroupTheory/ArchimedeanDensely): linear ordered group subsets are WF if discrete

  #18481 opened Oct 31, 2024

• feat(RingTheory/Valuation/Integers): `dvdNotUnit_iff_lt`

  #18482 opened Oct 31, 2024

• feat: `IsCoprime.wronskian_eq_zero_iff`

  #18483 opened Oct 31, 2024

• feat(Tactic): Tactic for computing asymptotics of real functions

  #18486 opened Oct 31, 2024

• feat(Analysis/PolarCoord): add versions for Lebesgue integral

  #18490 opened Oct 31, 2024

• feat: prepare for removing @[simp] from Sum.forall and Sum.exists

  #18491 opened Oct 31, 2024

• feat(Algebra): `Submodule R A` is algebra over `Ideal A`

  #18493 opened Oct 31, 2024

• fix: make sure that a MeasurableSpace instance uses Discreteness

  #18494 opened Oct 31, 2024

• feat: totally unimodular matrices

  #18495 opened Oct 31, 2024

• feat(Condensed): light condensed abelian groups satisfy countable AB4*

  #18497 opened Oct 31, 2024

• RFC chore: do not import `Tactic.Common` in Mathlib

  #18498 opened Oct 31, 2024

• feat(AlgebraicTopology/SimplicialSet): paths and the strict segal condition

  #18499 opened Oct 31, 2024

• feat(Algebra/Homology): the functoriality of the extension of complexes

  #18500 opened Oct 31, 2024

• feat(Algebra/Homology): the stupid truncation of homological complexes

  #18501 opened Oct 31, 2024

• feat(Algebra/Homology): the left homology of an extension of homological complexes

  #18502 opened Oct 31, 2024

• refactor: generalize results about `LinearIndependent` to `Semiring`

  #18503 opened Nov 1, 2024

• feat: approximate units in C⋆-algebras

  #18506 opened Nov 1, 2024

• chore(OperatorNorm/Completeness): drop a duplicate instance

  #18508 opened Nov 1, 2024

• feat(CategoryTheory/Abelian/GrothendieckAxioms): introduce grothendieck categories

  #18510 opened Nov 1, 2024

• chore: generalize conditions for colimitLimitIso

  #18511 opened Nov 1, 2024

• feat(FieldTheory/Adjoin): add `IntermediateField.mem_adjoin_range_iff`

  #18513 opened Nov 1, 2024

• feat(LinearAlgebra/TensorProduct/Field): some results on fields whose proof requires tensor product

  #18515 opened Nov 1, 2024

• chore: refactor roots of unity to avoid PNat

  #18516 opened Nov 1, 2024

• chore(RingTheory/NonUnitalSubring): split Basic.lean

  #18518 opened Nov 1, 2024

• chore(Algebra/Ring/Subsemiring): split `Basic.lean`

  #18519 opened Nov 1, 2024

• chore(Algebra/Ring/Subring): split `Basic.lean`

  #18520 opened Nov 1, 2024

• feat: `colim` preserves limits in functor categories

  #18521 opened Nov 1, 2024

• feat: towards equalizers in the category of ind-objects

  #18522 opened Nov 1, 2024

• Advances sorrys in ValuativeRing

  #18523 opened Nov 1, 2024

• chore(Algebra/Ring/Int): split `Algebra/Ring/Int.lean` into `Defs.lean` and `Basic.lean`

  #18526 opened Nov 1, 2024

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

  #18527 opened Nov 1, 2024

• chore(Algebra/Field): split `Subfield.lean` into `Defs` and `Basic`

  #18528 opened Nov 1, 2024

• refactor(AlgebraicGeometry/EllipticCurve/*): add `WeierstrassCurve.IsElliptic` and remove `EllipticCurve`

  #18531 opened Nov 1, 2024

• feat(CategoryTheory): Every colimit is a colimit on the Grothendieck construction on costructured arrows

  #18532 opened Nov 1, 2024

• feat(LinearAlgebra/PiTensorProduct): dependent version of tmulEquiv

  #18534 opened Nov 1, 2024

• refactor(Multiset): drop `Multiset.Disjoint`

  #18535 opened Nov 1, 2024

• feat(RingTheory): towards openness of flat locus

  #18536 opened Nov 1, 2024

• fix(FieldTheory/IntermediateField/Basic): fix typos in comment

  #18539 opened Nov 2, 2024

• feat: generalize `tendsto_measure_iInter`

  #18540 opened Nov 2, 2024

• feat(SetTheory/Cardinal/Arithmetic): fix namespace of `mk_iUnion_Ordinal_le_of_le`

  #18541 opened Nov 2, 2024

• feat(SetTheory/Cardinal/Aleph): some lemmas on `omega`

  #18542 opened Nov 2, 2024

• doc(Logic/Small/Defs): document `Small.{u, max u v}` instance

  #18544 opened Nov 2, 2024

• feat(Data/Real/Cardinality): `Uncountable ℝ`

  #18546 opened Nov 2, 2024

• feat: uncountable instances for `Ordinal` and isomorphic types

  #18547 opened Nov 2, 2024

• feat(Cache): include MathlibTest in the cache

  #18550 opened Nov 2, 2024

• feat(AlgebraicGeometry): the algebraic De Rham complex

  #18551 opened Nov 2, 2024

• feat: require that real or complex models with corners have convex interior

  #18554 opened Nov 2, 2024

• feat: lemmas about Finsupp.mapRange

  #18556 opened Nov 2, 2024

• feat: `Countable` deriving handler

  #18557 opened Nov 2, 2024

• chore: all variants of `limitOpIsoOpColimit`

  #18558 opened Nov 2, 2024

• feat: define restriction of perfect pairings

  #18559 opened Nov 2, 2024

• feat(RingTheory/Invariant): Define invariant extensions of rings

  #18560 opened Nov 2, 2024

• feat(InfiniteSum): add `Multipliable.congr'`

  #18561 opened Nov 2, 2024

• feat(RingTheory/Ideal/Over): Action of stabilizer on quotient

  #18562 opened Nov 2, 2024

• feat (Algebra/FreeMonoid) : free monoids over isomorphic types are isomorphic

  #18563 opened Nov 2, 2024

• feat: `Encodable` deriving handler

  #18564 opened Nov 3, 2024

• chore: `Pi.single` and `MultilinearMap.piFamily`

  #18566 opened Nov 3, 2024

• feat(Topology/Order): add more `CovBy.nhdsWithin...` lemmas

  #18567 opened Nov 3, 2024

• refactor(Algebra/Order/ZeroLE): typeclass for `0` / `1` being a bottom element

  #18568 opened Nov 3, 2024

• feat (LinearAlgebra/RootSystem/Finite): nondegeneracy of canonical bilinear form restricted to root span

  #18569 opened Nov 3, 2024

• feat(Algebra): add `IsLocalizedModule.liftOfLE`

  #18570 opened Nov 3, 2024

• chore(OnePoint): use `induction_eliminator`

  #18571 opened Nov 3, 2024

• refactor(GroupTheory/Sylow): Add version of `Sylow.not_dvd_index` with only typeclass assumptions

  #18572 opened Nov 3, 2024

• feat(GroupTheory/Sylow): A p-subgroup with index indivisible by p is a Sylow p-subgroup

  #18573 opened Nov 3, 2024

• feat(GroupTheory/SpecificGroups/ZGroup): Predicate for groups whose Sylow subgroups are all cyclic

  #18575 opened Nov 3, 2024

• chore: update Mathlib dependencies 2024-11-03

  #18576 opened Nov 3, 2024

• feat(CategoryTheory/Generator): introduce classes HasDetector and HasSeparator

  #18577 opened Nov 3, 2024

• feature(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map

  #18578 opened Nov 3, 2024

• feat(Rat/Denumerable): Use continued fractions for denumerability

  #18580 opened Nov 3, 2024

• feat(Data/PNat): two lemmas about sub

  #18581 opened Nov 3, 2024

• feat (Algebra/FreeMonoid/Basic) : length three

  #18582 opened Nov 3, 2024

• feat: whiskering of exact functors

  #18583 opened Nov 3, 2024

• chore(Rat/Cardinal): reduce imports and create new file

  #18584 opened Nov 3, 2024

• chore: dualize `IndYoneda`

  #18585 opened Nov 3, 2024

• doc: refer to `map_map_of_aemeasurable` in the docstring of `map_map`

  #18586 opened Nov 3, 2024

• feat(RingTheory/Jacobson): finite type algebras over jacobson rings are jacobson

  #18587 opened Nov 3, 2024

1 Issue opened by 1 person

• Hermite functions

  #18548 opened Nov 2, 2024

240 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(FieldTheory.JacobsonNoether) : add proof of the Jacobson-Noether theorem

  #16525 commented on Nov 2, 2024 • 67 new comments

• feat(GroupTheory/Congruence): simp lemmas for comap equivalences

  #17195 commented on Nov 3, 2024 • 30 new comments

• feat: quantales

  #17289 commented on Nov 2, 2024 • 24 new comments

• feat: combinatorial part of the Faa di Bruno formula

  #17169 commented on Nov 2, 2024 • 23 new comments

• feat: presented monoids

  #13152 commented on Nov 2, 2024 • 22 new comments

• feat: Mason-Stothers theorem (polynomial ABC)

  #15706 commented on Oct 31, 2024 • 22 new comments

• feat(Data/Multiset/Order): add Dershowitz-Manna Ordering and Theorem

  #14411 commented on Nov 1, 2024 • 16 new comments

• feat (Mathlib/RingTheory/MvPolynomial/Groebner) : monomial orders and division

  #16584 commented on Nov 1, 2024 • 15 new comments

• feat: check that every file imports Mathlib.Init

  #18281 commented on Nov 2, 2024 • 13 new comments

• feat(LocalRing/MaximalIdeal/Basic): localization of a Krull dim zero ring

  #17549 commented on Nov 2, 2024 • 12 new comments

• feat(Combinatorics/SimpleGraph): Add definition of disjoint sum of graphs

  #15546 commented on Nov 3, 2024 • 12 new comments

• feat(FiberedCategory/HasFibers): define HasFibers class

  #13611 commented on Oct 30, 2024 • 11 new comments

• feat: define singular `n`-manifolds

  #15906 commented on Nov 2, 2024 • 10 new comments

• feat(Combinatorics/Enumerative/Bell): number of ways of partitioning a set into subsets of given cardinalities

  #15644 commented on Nov 1, 2024 • 9 new comments

• feat: add results on cardinality of localization

  #18004 commented on Oct 31, 2024 • 9 new comments

• feat: sufficient condition for a presheaf to preserve finite limits

  #18283 commented on Oct 31, 2024 • 9 new comments

• feat(Algebra/MvPolynomial): Schwartz-Zippel lemma

  #5297 commented on Nov 3, 2024 • 9 new comments

• feat(SetTheory/Cardinal/Ordinal): sum_eq_iSup

  #16910 commented on Nov 2, 2024 • 8 new comments

• feat(RingTheory.MvPowerSeries.Topology): define the product topology on mv power series

  #14866 commented on Nov 1, 2024 • 8 new comments

• feat: Defining Greedoid

  #10186 commented on Nov 3, 2024 • 7 new comments

• refactor(NumberTheory/RamificationInertia): use `Ideal.LiesOver` in some results about `inertiaDeg`

  #18270 commented on Nov 3, 2024 • 7 new comments

• feat(NumberTheory/EllipticDivisibilitySequence): extend even-odd recursion to integers

  #13786 commented on Oct 28, 2024 • 7 new comments

• feat: quotient lift on a finite family

  #5576 commented on Nov 2, 2024 • 7 new comments

• feat: more on central simple algebras

  #17789 commented on Oct 30, 2024 • 6 new comments

• feat(Algebra/Category/ModuleCat): the pseudofunctors which send a ring to its category of modules

  #18197 commented on Nov 1, 2024 • 6 new comments

• feat: bounds for modular forms of non-positive weights

  #18192 commented on Oct 31, 2024 • 6 new comments

• feat(GroupTheory/GroupAction/Primitive)

  #12052 commented on Nov 1, 2024 • 6 new comments

• feat(Analysis): integer complement in `ℂ`

  #16542 commented on Oct 28, 2024 • 6 new comments

• refactor (LinearAlgebra/FreeProduct): move PowerAlgebra construction to its own namespace, minor simp opts

  #15686 commented on Nov 1, 2024 • 6 new comments

• feat(LinearAlgebra/Multilinear/DirectSum, LinearAlgebra/DirectSum/{PiTensorProduct,Finsupp}): interaction between `MultilinearMap` and `DirectSum`, and between `PiTensorProduct` and `DirectSum`

  #11155 commented on Nov 3, 2024 • 6 new comments

• feat(Combinatorics/SimpleGraph): conversions between `SimpleGraph` and `Digraphs`

  #16954 commented on Nov 3, 2024 • 6 new comments

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

  #16801 commented on Nov 1, 2024 • 6 new comments

• feat(Topology/ContinuousMap/Interval): define the concatenation operation on continuous maps on intervals as a continuous map

  #17621 commented on Oct 30, 2024 • 5 new comments

• feat(RingTheory/IntegralClosure/IsIntegralClosure/Basic): Add lemmas about MvPolynomial and Polynomial

  #18244 commented on Nov 2, 2024 • 5 new comments

• feat: Define `Nat.finMulAntidiagonal`, the `Finset` of tuples of naturals with a fixed product.

  #10668 commented on Nov 2, 2024 • 5 new comments

• feat(SetTheory/Game/Birthday): games with bounded birthday are a small set

  #16595 commented on Nov 2, 2024 • 5 new comments

• feat(SetTheory/Ordinal/CantorNormalForm): induct on base `ω` CNF

  #15991 commented on Nov 2, 2024 • 4 new comments

• feat: iterate derivative of finset sum

  #17853 commented on Oct 31, 2024 • 4 new comments

• refactor(SetTheory/ZFC/Basic): redefine `Definable`

  #16398 commented on Nov 2, 2024 • 4 new comments

• feat: prove Cauchy's upper bound on polynomial roots

  #16597 commented on Nov 3, 2024 • 4 new comments

• feat(Algebra/Category): for ring homs, epi + finite => surjective

  #18267 commented on Nov 2, 2024 • 4 new comments

• feat(FieldTheory/Minpoly): minpoly K x splits implies minpoly K (algebraMap K L a - x) splits

  #17369 commented on Nov 3, 2024 • 4 new comments

• feat: warn on `autoImplicit true`

  #17109 commented on Nov 2, 2024 • 3 new comments

• chore(SetTheory/Ordinal/FixedPointApproximants): golf + better variable management

  #16361 commented on Nov 2, 2024 • 3 new comments

• feat: define `IsLittleOTVS`

  #9675 commented on Oct 31, 2024 • 3 new comments

• feat: add `Decidable`, `Fintype`, `Encodable` linters

  #10235 commented on Nov 3, 2024 • 3 new comments

• feat(AlgebraicTopology/Nerve): nerve is 2-coskeletal

  #16782 commented on Oct 31, 2024 • 3 new comments

• chore(Tactic/Polyrith): remove polyrith dependency on Python

  #17626 commented on Nov 1, 2024 • 3 new comments

• feat(Algebra/Module): snake lemma

  #17948 commented on Nov 2, 2024 • 3 new comments

• feat(Algebra/Category/ModuleCat/Presheaf): presheaves of modules are generated by their sections

  #18160 commented on Oct 31, 2024 • 3 new comments

• feat(Analysis/NormedSpace/FunctionSeries): add eventually versions

  #16543 commented on Nov 2, 2024 • 2 new comments

• feat: define `ApproximateUnit` and basic API

  #17787 commented on Nov 1, 2024 • 2 new comments

• chore: import the `header` linter in all files imported in Mathlib.Init

  #18275 commented on Nov 2, 2024 • 2 new comments

• feat(Bicategory/Oplax): Fix simp lemmas and renaming

  #18252 commented on Oct 30, 2024 • 2 new comments

• feat(AlgebraicGeometry): pre-requisites of description of topological space of pullback

  #18255 commented on Oct 28, 2024 • 2 new comments

• feat(Fin/Parity): add `Fin.even_iff`

  #8960 commented on Nov 1, 2024 • 2 new comments

• feat(RingTheory/Valuation): valuation integers ring is a Principal Ideal ring iff the valuation range is not densely ordered

  #16619 commented on Nov 3, 2024 • 2 new comments

• feat(SetTheory/Game/PGame): Improve `insertLeft` / `insertRight` API

  #15779 commented on Oct 30, 2024 • 2 new comments

• feat(Data/Finset & List): Add Lemmas for Sorting and Filtering

  #9605 commented on Oct 30, 2024 • 2 new comments

• feat(RingTheory/LocalProperties): being projective can be checked locally on stalks

  #18131 commented on Nov 1, 2024 • 2 new comments

• feat: add two limit results

  #16545 commented on Oct 28, 2024 • 2 new comments

• feat(Computability): r.e. sets are closed under inter/union/projection/composition

  #16705 commented on Oct 31, 2024 • 2 new comments

• feat: `Finpartition.attachEquiv`

  #16835 commented on Nov 1, 2024 • 2 new comments

• feat(Sym2): Add pmap

  #16557 commented on Nov 1, 2024 • 2 new comments

• feat: `#guard_exceptions` -- like `#guard_msgs` but for parsers

  #16305 commented on Oct 31, 2024 • 2 new comments

• feat(Combinatorics/SimpleGraph/Matching): graph isomorphisms preserve matchings

  #17436 commented on Nov 2, 2024 • 2 new comments

• chore(SetTheory/ZFC/Rank): clean up file

  #18239 commented on Oct 31, 2024 • 2 new comments

• feat(Analysis/Complex/AbsMax): add two lemmas

  #18198 commented on Nov 3, 2024 • 2 new comments

• feat(CategoryTheory): codiscrete categories

  #17174 commented on Oct 31, 2024 • 2 new comments

• feat(AlgebraicTopology/HomotopyCat): SSet.hoFunctor

  #16783 commented on Oct 29, 2024 • 2 new comments

• feat: compare PR `olean`s size with `master`

  #16020 commented on Nov 2, 2024 • 1 new comment

• feat(LinearAlgebra/Matrix): characterize Jacobson radicals in matrix rings

  #17756 commented on Nov 2, 2024 • 1 new comment

• feat: add Dockerfiles for lean and mathlib

  #15936 commented on Nov 2, 2024 • 1 new comment

• chore(SetTheory/Ordinal/CantorNormalForm): `CNF.exponents` and `CNF.coeffs`

  #15915 commented on Oct 31, 2024 • 1 new comment

• feat(Order/Hom/Basic): `WithBot (Fin n) ≃o Fin (n + 1)`

  #18210 commented on Nov 3, 2024 • 1 new comment

• feat(SimpleGraph): independent sets

  #18218 commented on Nov 1, 2024 • 1 new comment

• feat(Data/Vector): add `pmap` for vectors and prove some lemmas

  #17189 commented on Nov 3, 2024 • 1 new comment

• feat(Order/Bounds/Basic): Add basic order lemmas

  #17595 commented on Nov 2, 2024 • 1 new comment

• feat(Topology/PartitionOfUnity): add variations of partition of unity for locally compact T2 space

  #12266 commented on Nov 2, 2024 • 1 new comment

• feat(NumberField/CanonicalEmbedding): put an euclidean space structure on the mixed space

  #18245 commented on Oct 29, 2024 • 1 new comment

• feat(Data/List/SplitLengths): splitting a list to chunks of given sizes

  #17191 commented on Nov 2, 2024 • 1 new comment

• feat(RingTheory/Derivation/MapCoeffs): define `mapCoeffs` on a differential ring

  #14967 commented on Oct 29, 2024 • 1 new comment

• feat(Order/InitialSeg): extra lemmas on `α ≤i β`

  #17632 commented on Nov 3, 2024 • 1 new comment

• feat(RingTheory/SimpleRing/Basic): characterise simple ring in terms of injectiveness

  #18113 commented on Oct 28, 2024 • 1 new comment

• doc: factorial notation docstring

  #18085 commented on Oct 28, 2024 • 1 new comment

• feat (Probability.Kernel): Add definitions and API for `Kernel.fst'` and `snd'`

  #15466 commented on Oct 31, 2024 • 1 new comment

• feat(Combinatorics/Additive): small tripling implies small powers

  #18084 commented on Nov 1, 2024 • 1 new comment

• chore(SetTheory/Ordinal/Basic): deprecate `List.Sorted.lt_ord_of_lt`

  #16966 commented on Oct 31, 2024 • 1 new comment

• feat(LinearAlgebra/{TensorProductBasis,Dual}): basis and dual of `PiTensorProduct`

  #11156 commented on Nov 3, 2024 • 1 new comment

• feat(SetTheory/Ordinal/Arithmetic): make `IsNormal` a structure

  #17746 commented on Oct 30, 2024 • 0 new comments

• feat(Order/Filer/ENNReal): add Real.limsup_mul_le

  #18172 commented on Nov 1, 2024 • 0 new comments

• feat(Computability/ContextFreeGrammar): closure under union

  #13514 commented on Nov 2, 2024 • 0 new comments

• refactor: make `CanonicallyOrdered...` mixin

  #17444 commented on Oct 28, 2024 • 0 new comments

• feat: lint on declarations mentioning `Invertible` or `Unique`

  #17518 commented on Nov 2, 2024 • 0 new comments

• feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation

  #17522 commented on Oct 31, 2024 • 0 new comments

• feat(Algebra/MvPolynomial/Degrees): degreeOf_mul_X_eq_degreeOf_add_one_iff

  #17553 commented on Nov 1, 2024 • 0 new comments

• feat: rewrite the duplicateImports linter

  #17555 commented on Nov 2, 2024 • 0 new comments

• chore(Algebra/Order/GroupWithZero/Unbundled): deprecate useless lemmas, use `ZeroLEOneClass`

  #17593 commented on Nov 2, 2024 • 0 new comments

• chore(Order/InitialSeg): fix simp lemmas

  #17602 commented on Oct 30, 2024 • 0 new comments

• feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas

  #17623 commented on Nov 3, 2024 • 0 new comments

• feat: universal properties of vector bundle constructions

  #17627 commented on Oct 29, 2024 • 0 new comments

• chore(Linter/TextBased): simplify comparison of style exceptions

  #17662 commented on Nov 2, 2024 • 0 new comments

• feat: derivatives of piLp operations

  #17665 commented on Oct 31, 2024 • 0 new comments

• refactor: turn `IsTorsionFree` into a typeclass

  #17672 commented on Oct 29, 2024 • 0 new comments

• feat: Set to Function

  #17686 commented on Oct 28, 2024 • 0 new comments

• refactor: generalize Mul of Submodule and SMul of Ideal on Submodule to noncommutative setting

  #17708 commented on Oct 30, 2024 • 0 new comments

• feat: the unusedVariableCommand linter

  #17715 commented on Oct 31, 2024 • 0 new comments

• WIP: Frobenius Elements

  #17717 commented on Nov 3, 2024 • 0 new comments

• feat(Analysis/Normed/Ring/Seminorm): add lemmas

  #18173 commented on Nov 3, 2024 • 0 new comments

• chore(Nat.Factorization): rename `ord_proj/compl` -> `ordProj/Compl`

  #18191 commented on Nov 3, 2024 • 0 new comments

• feat(Algebra): define `PrimitiveIdempotents`

  #18195 commented on Oct 29, 2024 • 0 new comments

• refactor(MeasureTheory/MeasurableSpace/Card): avoid `Ordinal.toType`

  #18199 commented on Nov 2, 2024 • 0 new comments

• chore: refactor algebraic filter bases

  #18202 commented on Oct 30, 2024 • 0 new comments

• feat(SetTheory/Cardinal/Aleph): `range aleph = Ici ℵ₀`

  #18203 commented on Nov 1, 2024 • 0 new comments

• chore(SetTheory/Cardinal/Aleph): golf `aleph` theorems

  #18204 commented on Nov 1, 2024 • 0 new comments

• chore(SetTheory/Ordinal/Basic): golf/clean up `Cardinal.ord` theorems

  #18206 commented on Oct 30, 2024 • 0 new comments

• feat(Order/Cofinal): predicate for cofinal sets

  #18214 commented on Nov 2, 2024 • 0 new comments

• chore(*): `LinearOrder` + `IsWellOrder α (· < ·)` → `LinearOrder` + `WellFoundedLT`

  #18217 commented on Oct 30, 2024 • 0 new comments

• refactor(Order/WellFounded): deprecate `WellFounded.succ`

  #18238 commented on Oct 30, 2024 • 0 new comments

• refactor(RingTheory/Ideal/Pointwise): Make `Ideal.IsPrime.smul` into an instance

  #18241 commented on Oct 28, 2024 • 0 new comments

• feat(RingTheory/NoetherNormalization):Add noether normalization lemma

  #18247 commented on Nov 1, 2024 • 0 new comments

• feat(Algebra/Category/ModuleCat): exterior power functors on `ModuleCat`

  #18261 commented on Oct 27, 2024 • 0 new comments

• Feat: Second-derivative test from calculus

  #18266 commented on Nov 3, 2024 • 0 new comments

• feat(Topology/Sheaves/Stalks): Generalize to `stalkPushforward_iso_of_inducing`

  #18268 commented on Oct 28, 2024 • 0 new comments

• feat(AlgebraicGeometry): relative gluing of schemes

  #18284 commented on Nov 2, 2024 • 0 new comments

• feat(Wiedijk100Theorems): roots of a quartic

  #18290 commented on Oct 28, 2024 • 0 new comments

• feat(ProbabilityMeasure): continuity of integral against a bounded continuous function

  #18292 commented on Nov 3, 2024 • 0 new comments

• perf: make `Mul.toSMul` higher priority

  #18294 commented on Oct 28, 2024 • 0 new comments

• feat(SetTheory/Ordinal/ENat): `Ordinal.toENat`

  #17758 commented on Nov 2, 2024 • 0 new comments

• feat(SetTheory/Ordinal/Veblen): the Veblen hierarchy

  #17802 commented on Nov 1, 2024 • 0 new comments

• feat(SetTheory/Cardinal/Arithmetic): cardinality of ordinal exponential

  #17813 commented on Nov 2, 2024 • 0 new comments

• feat: induction principle for `ENNReal`-valued measurable functions from a sigma-finite space

  #17835 commented on Nov 2, 2024 • 0 new comments

• refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal

  #17904 commented on Oct 31, 2024 • 0 new comments

• feat(NumberTheory/NumberField): proof of the Analytic Class Number Formula

  #17914 commented on Nov 1, 2024 • 0 new comments

• chore: deprecate `Quotient.out'`

  #17941 commented on Oct 30, 2024 • 0 new comments

• feat(MeasureTheory): prove that some equivalences are measure preserving

  #17944 commented on Oct 29, 2024 • 0 new comments

• chore(Order/Intervals/Set): move some defs to a new file

  #17950 commented on Oct 28, 2024 • 0 new comments

• feat: inclusion-exclusion principle

  #17957 commented on Oct 27, 2024 • 0 new comments

• feature(Analysis/Convex/Topology): convex closed hull

  #17983 commented on Nov 1, 2024 • 0 new comments

• feat: the `#find_syntax` command

  #17986 commented on Oct 29, 2024 • 0 new comments

• chore(Order/InitialSeg): rename various defs

  #17989 commented on Oct 31, 2024 • 0 new comments

• chore(FieldTheory/RatFunc): clean up porting notes

  #18001 commented on Nov 3, 2024 • 0 new comments

• feat(CategoryTheory/Enriched): functor categories are enriched

  #18009 commented on Nov 1, 2024 • 0 new comments

• refactor(SetTheory/Cardinal/Cofinality): deprecate `StrictOrder.cof`

  #18043 commented on Nov 3, 2024 • 0 new comments

• feat: cardinalities in specific inverse systems

  #18067 commented on Oct 30, 2024 • 0 new comments

• feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot and succ cases)

  #18127 commented on Oct 28, 2024 • 0 new comments

• feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limit case)

  #18137 commented on Oct 27, 2024 • 0 new comments

• feat(Topology/Algebra/Field): `ContinuousSMul` for intermediate fields

  #18142 commented on Oct 28, 2024 • 0 new comments

• chore: import `Tactic.Positivity.Finset` in `Tactic.Positivity`

  #18146 commented on Nov 1, 2024 • 0 new comments

• feat: Hopf algebra structure on monoid algebras

  #13609 commented on Oct 27, 2024 • 0 new comments

• feat(Topology/Module): generalize `ContinuousLinearMap.compSL`

  #13648 commented on Nov 3, 2024 • 0 new comments

• feat(Topology/Order/HullKernel): Add the Hull-Kernel Topology

  #13918 commented on Nov 1, 2024 • 0 new comments

• feat(Bicategory/Functorbicategory): define bicategory of pseudofunctors

  #14089 commented on Oct 30, 2024 • 0 new comments

• feat(AlgebraicGeometry): representability by a scheme is a local property

  #14208 commented on Oct 27, 2024 • 0 new comments

• feat(RepresentationTheory/FdRep): FdRep is a full subcategory of Rep

  #14313 commented on Oct 30, 2024 • 0 new comments

• feat(Analysis/NormedSpace/MStructure): M-ideals

  #14369 commented on Nov 1, 2024 • 0 new comments

• feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat`

  #14486 commented on Nov 1, 2024 • 0 new comments

• chore: add typeclasses to unify various `add_top`, `add_eq_top`, etc.

  #14598 commented on Nov 2, 2024 • 0 new comments

• feat(Measure): add `gcongr` lemmas

  #14739 commented on Nov 3, 2024 • 0 new comments

• feat: Valuative criterion for properness.

  #14782 commented on Nov 2, 2024 • 0 new comments

• feat(MvPowerSeries.Order): order of multivariate power series

  #14983 commented on Oct 30, 2024 • 0 new comments

• feat(LinearAlgebra/QuadraticForm/Basic): weaken invertibility hypothesis on 2

  #14986 commented on Oct 30, 2024 • 0 new comments

• feat(Quot): add simple lemmas on function congruence

  #15127 commented on Oct 30, 2024 • 0 new comments

• feat(ENat): iSup_add

  #15344 commented on Nov 1, 2024 • 0 new comments

• feat(Analysis.Normed.Ring.Seminorm): add SmoothingSeminorm

  #15373 commented on Oct 28, 2024 • 0 new comments

• feature(Order/ScottContinuity): Scott Continuity on product spaces

  #15412 commented on Nov 1, 2024 • 0 new comments

• feat(Computability.Timed): Formalization of runtime complexity of insertion sort

  #15449 commented on Nov 1, 2024 • 0 new comments

• feat(Computability.Timed): Formalization of runtime complexity of List.merge

  #15451 commented on Nov 1, 2024 • 0 new comments

• feat(Computability.Timed): Formalization of runtime complexity of List.mergeSort

  #15452 commented on Nov 1, 2024 • 0 new comments

• feat(Data/FinEnum): Option instance and Type recursor

  #15647 commented on Oct 28, 2024 • 0 new comments

• feat(Computability): introduce Generalised NFA as bridge to Regular Expression

  #15649 commented on Oct 28, 2024 • 0 new comments

• Improving the performance of typeclass inference

  #16644 commented on Oct 30, 2024 • 0 new comments

• Tracking Issue: Combinatorial Game Theory

  #18161 commented on Oct 30, 2024 • 0 new comments

• WIP: feat(GroupTheory/GroupAction/Basic): add pointwise and setwise stabilizers

  #6533 commented on Oct 29, 2024 • 0 new comments

• feat: Lindemann-Weierstrass Theorem

  #6718 commented on Nov 3, 2024 • 0 new comments

• chore: rename `Pi.fintype` to `Pi.instFintype`

  #7850 commented on Oct 30, 2024 • 0 new comments

• perf: reorder `extends` and change instance priority in algebra hierarchy

  #7873 commented on Oct 30, 2024 • 0 new comments

• Add `NormedSpace.Alternating`

  #8691 commented on Nov 3, 2024 • 0 new comments

• refactor(LinearAlgebra/Matrix/SesquilinearForm): Sesquilinear Maps and Scalar Matrices

  #9353 commented on Nov 1, 2024 • 0 new comments

• feat(FieldTheory/LinearDisjoint): definition and basic properties of linearly disjoint of fields

  #9651 commented on Nov 1, 2024 • 0 new comments

• feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties

  #10654 commented on Nov 3, 2024 • 0 new comments

• feat: monoidal category structure on bialgebras

  #11978 commented on Oct 27, 2024 • 0 new comments

• feat: tensor products of Hopf algebras

  #12009 commented on Oct 27, 2024 • 0 new comments

• feat: monoidal structure on Hopf algebras

  #12011 commented on Oct 27, 2024 • 0 new comments

• feat(GroupTheory/GroupAction/Iwasawa): the Iwasawa criterion for simplicity

  #12048 commented on Oct 31, 2024 • 0 new comments

• feat(GroupTheory/GroupAction/Primitive): lemmas about primitive actions for finite sets

  #12053 commented on Oct 29, 2024 • 0 new comments

• refactor(RingTheory/HahnSeries) : several generalizations

  #12251 commented on Oct 31, 2024 • 0 new comments

• feat(Analysis/BoxIntegral/UnitPartition): Prove results linking integral point counting and integrals

  #12405 commented on Oct 30, 2024 • 0 new comments

• feat (Lattice/Covolume): Add results linking point counting in lattices and covolume

  #12488 commented on Oct 30, 2024 • 0 new comments

• feat(CategoryTheory): the localized category is monoidal

  #12728 commented on Oct 29, 2024 • 0 new comments

• perf: decouple algebraic and order hierarchies in type class search

  #12778 commented on Nov 3, 2024 • 0 new comments

• feat(LinearAlgebra/UnitaryGroup): Add properties of Special Unitary Group

  #12799 commented on Oct 30, 2024 • 0 new comments

• chore: remove `CovariantClass` and `ContravariantClass`

  #13124 commented on Nov 3, 2024 • 0 new comments

• feat: basic concepts of auction theory

  #13248 commented on Oct 30, 2024 • 0 new comments

• feat(RingTheory/Derivation/Basic): define lifting a derivation via an algebra homomorphism

  #16792 commented on Oct 31, 2024 • 0 new comments

• feat(Data/List/GroupBy): characterization of `List.groupBy`

  #16837 commented on Oct 30, 2024 • 0 new comments

• feat: extend `linear_combination` to prove inequalities

  #16841 commented on Nov 2, 2024 • 0 new comments

• feat(SetTheory/Cardinal/Cofinality): Ordinal.IsFundamentalSequence.lt

  #16926 commented on Nov 2, 2024 • 0 new comments

• chore(SetTheory/Ordinal/Basic): group `typein` and `enum` theorems together

  #16963 commented on Oct 31, 2024 • 0 new comments

• feat(FieldTheory/Galois): Lemmas of galois theory

  #16979 commented on Oct 31, 2024 • 0 new comments

• feat(FieldTheory/Galois): Fundamental theorem of infinite galois theory

  #16982 commented on Nov 1, 2024 • 0 new comments

• feat(Topology/Group): Continuous isomorphism

  #16991 commented on Oct 31, 2024 • 0 new comments

• feat(Topology/Group/Profinite): Profinite group is limit of finite group

  #16992 commented on Oct 31, 2024 • 0 new comments

• feat(FieldTheory/Galois): Galois group is profinite

  #16993 commented on Oct 31, 2024 • 0 new comments

• feat(SetTheory/Cardinal/Regular): define singular cardinals

  #17005 commented on Oct 29, 2024 • 0 new comments

• feat(SetTheory/Game/Birthday): basic API for `Ordinal.toGame`

  #17015 commented on Nov 1, 2024 • 0 new comments

• feat: several results on permutations, cycles, etc

  #17046 commented on Oct 28, 2024 • 0 new comments

• feat(GroupTheory/SpecificGroups/Alternating/Centralizer): compute the centralizer of a permutation in the alternating group

  #17047 commented on Oct 30, 2024 • 0 new comments

• chore: add workflow for merging master into bump/v4.x.y branches

  #17081 commented on Oct 31, 2024 • 0 new comments

• feat: measurability of addition and multiplication on `EReal`

  #17097 commented on Oct 28, 2024 • 0 new comments

• feat(Data/List/RunLength): run-length encoding

  #17105 commented on Oct 30, 2024 • 0 new comments

• feat(Tactic/Linter): add unicode linter for unicode variant-selectors

  #17129 commented on Oct 31, 2024 • 0 new comments

• feat(Archive/Ioi/Ioi2024Q2): a proof of the solution of question 2 from IOI 2024.

  #17145 commented on Oct 31, 2024 • 0 new comments

• feat(RingTheory/PrimaryDecomposition): PIR of Noetherian under jacobson condition

  #17246 commented on Nov 1, 2024 • 0 new comments

• feat: Decomposing a submodule of a product

  #17308 commented on Nov 1, 2024 • 0 new comments

• feat(Counterexamples/DiscreteTopologyNonDiscreteUniformity): add a counterexample about discrete uniformity and Cauchy filters

  #17417 commented on Oct 30, 2024 • 0 new comments

• feat: generalize `Prod.wellFoundedLT/GT` to `Preorder`s

  #17435 commented on Nov 2, 2024 • 0 new comments

• feat(Computability): language-preserving maps between NFA and RE

  #15654 commented on Oct 28, 2024 • 0 new comments

• chore(Filter/Pi): add `piMap_map_pi`

  #15744 commented on Oct 31, 2024 • 0 new comments

• feat: generators for SL(2, Z)

  #15851 commented on Oct 28, 2024 • 0 new comments

• feat(SetTheory/Ordinal/Principal): more lemmas on additively principal ordinals

  #15989 commented on Nov 1, 2024 • 0 new comments

• chore(Topology): Namespace `Inducing`, `Embedding`...

  #15993 commented on Oct 29, 2024 • 0 new comments

• feat(UpperHalfPlane): weaken assumptions of multiple atImInfty lemmas

  #16015 commented on Oct 30, 2024 • 0 new comments

• feat: representatives for the `FixedDetMatrices` under SL action

  #16160 commented on Oct 31, 2024 • 0 new comments

• feat(Archive/Imo): formalize IMO 1982q3

  #16190 commented on Oct 28, 2024 • 0 new comments

• chore: deprime `induction, cases` in `Combinatorics`

  #16250 commented on Nov 3, 2024 • 0 new comments

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

  #16303 commented on Nov 1, 2024 • 0 new comments

• chore(Data/Quot): deprecate `ind*'` APIs

  #16314 commented on Oct 30, 2024 • 0 new comments

• feat(Analysis/Normed/Module/WeakDual): Banach Dieudonné Lemma

  #16316 commented on Nov 1, 2024 • 0 new comments

• feat: rewrite the trailing whitespace linter in Lean

  #16334 commented on Oct 31, 2024 • 0 new comments

• chore(Data/Quot): rename `surjective_*_mk` => `*.mk_surjective`

  #16410 commented on Nov 2, 2024 • 0 new comments

• feat: `QuotLike`

  #16421 commented on Nov 2, 2024 • 0 new comments

• test use `QuotLike` APIs

  #16428 commented on Nov 2, 2024 • 0 new comments

• chore(Computability/ContextFreeGrammar): replace `List` by `Finset`

  #16443 commented on Nov 2, 2024 • 0 new comments

• feat(KrullDimension): height_strictMono, mapping theorems

  #16555 commented on Nov 1, 2024 • 0 new comments

• feat(Analysis.InnerProductSpace): Decomposition of finite-dimensional inner product space as direct sum of joint eigenspaces of commuting finite tuples of symmetric operators

  #16569 commented on Nov 1, 2024 • 0 new comments

• perf: reorder `extends` of `(Add)Monoid`

  #16637 commented on Oct 30, 2024 • 0 new comments

• feat(Analysis/BoxIntegral): Add BoxPartition defined by subdivision of the integer lattice

  #16675 commented on Oct 31, 2024 • 0 new comments

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

  #16743 commented on Oct 30, 2024 • 0 new comments

• feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd`

  #16769 commented on Nov 2, 2024 • 0 new comments