4 Pull requests merged by 2 people

• Lean pr testing 6128

  #19273 merged Nov 21, 2024

• chore(RingTheory/Flat): tensor with localization preserves injectivity even over semirings

  #19165 merged Nov 20, 2024

• merge master

  #19208 merged Nov 18, 2024

• chore: use AlgHom.restrictDomain

  #19167 merged Nov 17, 2024

121 Pull requests opened by 53 people

• feat(RingTheory/LocalProperties): adapt #19080 to #19118

  #19126 opened Nov 16, 2024

• doc(GroupTheory/Commensurable): clarify some docstrings

  #19127 opened Nov 16, 2024

• feat: `#trans_import` shows the imports of the current module

  #19129 opened Nov 16, 2024

• chore(AlgebraicGeometry) add `Scheme.Hom.appTop`

  #19130 opened Nov 16, 2024

• feat: `isCoprime_mul_units_left`, `isCoprime_mul_units_right`

  #19133 opened Nov 16, 2024

• feat(CategoryTheory): left and right lifting properties

  #19135 opened Nov 16, 2024

• feat: handle scalar multiplication in `linear_combination`

  #19136 opened Nov 17, 2024

• feat(RingTheory/Ideal/Over): define the set of all prime ideals that lie over an ideal

  #19139 opened Nov 17, 2024

• feat(NumberTheory/RamificationInertia): `ramificationIdx` and `inertiaDeg` in Galois extensions

  #19141 opened Nov 17, 2024

• chore(SetTheory/Ordinal/Exponential): redefine ordinal exponential without `bsup`

  #19145 opened Nov 17, 2024

• feat: Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul

  #19146 opened Nov 17, 2024

• feat: add `ENat.map` and lemmas

  #19149 opened Nov 17, 2024

• feat(Order/Bounds/Lattice): Bounds over collections of sets

  #19150 opened Nov 17, 2024

• feat: coproducts in the category of Ind-objects

  #19154 opened Nov 17, 2024

• feat(AlgebraicTopology): model categories

  #19158 opened Nov 17, 2024

• feat(Polynomial): bounding the coefficients of `modByMonic`/`divByMonic`

  #19163 opened Nov 17, 2024

• Add `toWithTop`, `ofWithTop`

  #19164 opened Nov 17, 2024

• feat(Analysis/Convex/Topology): closure of interior and interior of closure for a convex set

  #19170 opened Nov 17, 2024

• feat: additivize equivariance of morphisms of actions

  #19171 opened Nov 17, 2024

• test: the findDefEqAbuse linter

  #19177 opened Nov 18, 2024

• feat: add Nat.digits_base_pow_mul and Nat.digits_append_zeroes_append_digits

  #19179 opened Nov 18, 2024

• feat(GroupTheory/SpecificGroups/Cyclic): Cardinality of automorphism group

  #19180 opened Nov 18, 2024

• feat(SetTheory/Ordinal/Arithmetic): order isomorphism between omega and the natural numbers

  #19189 opened Nov 18, 2024

• refactor: make `LinearOrderedCommMonoidWithZero` extend `OrderBot`

  #19193 opened Nov 18, 2024

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

  #19198 opened Nov 18, 2024

• feat(CategoryTheory): split up a product into a binary product

  #19199 opened Nov 18, 2024

• feat(CategoryTheory): expand the API for AB axioms

  #19200 opened Nov 18, 2024

• feat(MvPolynomial): more lemmas about `finSuccEquiv`

  #19201 opened Nov 18, 2024

• feat(Algebra/Homology): API for the homology of an extension of homological complex

  #19203 opened Nov 18, 2024

• chore(Data/Finsupp): split off basic scalar multiplication

  #19205 opened Nov 18, 2024

• feat(LinearAlgebra): add a variable_alias for VectorSpace

  #19212 opened Nov 18, 2024

• feat(Algebra/Category): `Under.pushout f` is left-exact if `f` is flat.

  #19213 opened Nov 18, 2024

• feat: expand API for `CFC.posPart`

  #19221 opened Nov 18, 2024

• feat(Order/Directed): DirectedOn and products

  #19222 opened Nov 18, 2024

• fix(CI): unwrap `lake test` in problem matcher

  #19227 opened Nov 18, 2024

• feat: add bundled multiplication maps for matrices

  #19229 opened Nov 18, 2024

• refactor(Algebra/Bilinear): generalize to non-commutative base rings

  #19232 opened Nov 18, 2024

• feat(CategoryTheory): retracts of objects and morphisms

  #19233 opened Nov 19, 2024

• refactor(SetTheory/Ordinal/NaturalOps): redefine natural addition without `blsub`

  #19236 opened Nov 19, 2024

• chore(SetTheory/Ordinal/NaturalOps): address porting notes

  #19237 opened Nov 19, 2024

• refactor(Nat.Prime.Defs): use `csimp` for `Nat.decidablePrime`

  #19240 opened Nov 19, 2024

• feat: generalize `Ideal.spanNorm` to allow non free extensions

  #19244 opened Nov 19, 2024

• feat: algebraic properties of `Finset.sup`

  #19245 opened Nov 19, 2024

• feat: `MulLeftMono` implies `PosMulMono`

  #19248 opened Nov 19, 2024

• feat(Combinatorics/SimpleGraph/Matching): add `IsCycles` and `IsAlternating` with basic results

  #19250 opened Nov 19, 2024

• feat(Pointwise): monotonicity of `pow`

  #19252 opened Nov 19, 2024

• Do not merge: Performance of SemigroupAction against nightly-testing

  #19257 opened Nov 19, 2024

• feat: `S ^ n = S` where `S` is a submonoid

  #19259 opened Nov 19, 2024

• feat(CategoryTheory/SmallObject/Iteration): existence of objects (limit case)

  #19264 opened Nov 19, 2024

• doc(SetTheory/ZFC/Ordinal): add docstrings to lemmas on transitive sets

  #19266 opened Nov 19, 2024

• feat(AlgebraicTopology): StrictSegal simplicial sets are quasicategories

  #19270 opened Nov 19, 2024

• feat(CategoryTheory): pushforward pullback adjunction for `P.Over Q X`

  #19271 opened Nov 19, 2024

• fix: if nolint files change, do a full rebuild

  #19275 opened Nov 20, 2024

• chore(Order/ConditionallyCompleteLattice): split off `Defs.lean` from `Basic.lean`

  #19277 opened Nov 20, 2024

• chore(MeasureTheory): remove the dependence of the Lebesgue decomposition on Bochner integrals

  #19278 opened Nov 20, 2024

• Split polynomial.algebra

  #19281 opened Nov 20, 2024

• add a variable_alias for Quantale and AddQuantale

  #19282 opened Nov 20, 2024

• test: commit a change only to the "master" CI build action

  #19284 opened Nov 20, 2024

• feat: more `bound` lemmas

  #19285 opened Nov 20, 2024

• feat(NumberTheory): Abel summation

  #19289 opened Nov 20, 2024

• feat: quantale homomorphisms

  #19291 opened Nov 20, 2024

• feat: more `eLpNorm` API

  #19293 opened Nov 20, 2024

• chore: remove the `Smooth` alias for infinitely differentiable functions between manifolds

  #19296 opened Nov 20, 2024

• feat(to_additive): option to not translate operations on a type

  #19297 opened Nov 20, 2024

• feat(Algebra/Vertex): Define vertex operators

  #19298 opened Nov 20, 2024

• feat(Algebra/CategoryTheory): Add CommAlgebraCat

  #19299 opened Nov 20, 2024

• fix(to_additive): automatically translate all instances generated by `extends`

  #19302 opened Nov 20, 2024

• feat(RingTheory/Polynomial/Hilbert): the definition of the Hilbert polynomial in terms of a natural number `d` and a polynomial `p : ℤ[X]`

  #19303 opened Nov 20, 2024

• feat(CategoryTheory/MorphismProperty): classes of morphisms that are stable under transfinite compositions

  #19306 opened Nov 20, 2024

• feat(LinearAlgebra/Matrix/Permanent): smul

  #19307 opened Nov 20, 2024

• chore(RingTheory/Localization): golfs and generalizations

  #19310 opened Nov 20, 2024

• feat: Sedrakyan's lemma

  #19311 opened Nov 20, 2024

• feat(CategoryTheory/Over): more API for `post`

  #19312 opened Nov 20, 2024

• feat(Finsupp/Fin): Add `Finsupp` operations on `Fin` tuples

  #19315 opened Nov 21, 2024

• Test importing topology in ordinal

  #19320 opened Nov 21, 2024

• chore: change associativity of `+ᵥ` from `infixl` to `infixr`

  #19321 opened Nov 21, 2024

• test: rebuild modifying lint

  #19322 opened Nov 21, 2024

• feat: Function to Sum decomposition

  #19323 opened Nov 21, 2024

• style(Computability/ContextFreeGrammar/reverse): injective and surjec…

  #19325 opened Nov 21, 2024

• perf(CI): automatically benchmark PRs when they are opened

  #19329 opened Nov 21, 2024

• feat(CategoryTheory): construction of sections of functors by transfinite induction

  #19330 opened Nov 21, 2024

• feat(Data/Finsupp): generalise `Finsupp` to any "zero" value

  #19337 opened Nov 21, 2024

• feat(NumberTheory/Padics): Mahler coeffs tend to 0

  #19340 opened Nov 21, 2024

• chore: split out Algebra.GroupWithZero.Nat

  #19342 opened Nov 21, 2024

• feat(LinearAlgebra/RootSystem/Finite): Coxeter weights are bounded above by 4

  #19343 opened Nov 21, 2024

• chore: split notation typeclasses out of Algebra.Group.Defs

  #19350 opened Nov 22, 2024

• chore: change some `nlinarith`s to `linear_combination`s

  #19352 opened Nov 22, 2024

• chore: golf some term/rw proofs using `linear_combination`

  #19353 opened Nov 22, 2024

• chore: split Order.Filter.Basic, creating Order.Filter.Finite

  #19354 opened Nov 22, 2024

• feat: the pullback of a vector field in a vector space

  #19357 opened Nov 22, 2024

• chore(Filter): move defs of `Filter.IsBounded` etc

  #19358 opened Nov 22, 2024

• feat: locally compact manifolds are finite-dimensional

  #19362 opened Nov 22, 2024

• chore(RingTheory/Noetherian): further split `Defs.lean`

  #19364 opened Nov 22, 2024

• test: try emoji action

  #19367 opened Nov 22, 2024

• chore(RingTheory): split up `Algebraic.lean`

  #19370 opened Nov 22, 2024

• feat: trigger automated Zulip emojis via `bors x` command

  #19371 opened Nov 22, 2024

• find defeq abuse using diagnostics

  #19372 opened Nov 22, 2024

• feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn`

  #19373 opened Nov 22, 2024

• chore: avoid importing `ContDiff.Defs` in `FDeriv.Analytic`

  #19374 opened Nov 22, 2024

• chore(Algebra/Polynomial): don't import `Ideal` when defining `Polynomial.roots`

  #19376 opened Nov 22, 2024

• feat(Combinatorics/SimpleGraph): add lemmas about `spanningCoe`

  #19377 opened Nov 22, 2024

• feat: Explanation widgets

  #19378 opened Nov 22, 2024

• refactor(lint-style): make sure to read the nolints file outside of t…

  #19384 opened Nov 22, 2024

• feat: introduce the missing notation for `AddHom`

  #19387 opened Nov 22, 2024

• chore: make map_ofNat a simp lemma

  #19388 opened Nov 22, 2024

• feat: prove `zmodRepr` is unique

  #19391 opened Nov 23, 2024

• feat:(SetTheory/Game/PGame): down and up games

  #19393 opened Nov 23, 2024

• chore: more simpNF cleanup

  #19395 opened Nov 23, 2024

• feat(Algebra/Ring/Parity): Add lemma `odd_add_self_sub_one`

  #19397 opened Nov 23, 2024

• feat: `Icc a b + Icc c d = Icc (a + c) (b + d)`

  #19398 opened Nov 23, 2024

• feat(GroupTheory): some lemmas about blocks

  #19399 opened Nov 23, 2024

• feat: `s⁻¹.encard = s.encard`

  #19400 opened Nov 23, 2024

• chore: rename `forall_image2_iff` to `forall_mem_image2`

  #19401 opened Nov 23, 2024

• chore: rename `Codisjoint_comm` to `codisjoint_comm`

  #19403 opened Nov 23, 2024

• feat(RingTheory/Polynomial/Hilbert): given a natural number `d` and a polynomial `p : ℤ[X]`, proved the key property of the Hilbert polynomial in terms of `d` and `p`

  #19404 opened Nov 23, 2024

• chore(discover-lean-pr-testing): ignore stage0 PRs, more tracing

  #19405 opened Nov 23, 2024

• feat: `{a, b} * s = a • s ∪ b • s`

  #19406 opened Nov 23, 2024

• feat: `(t \ s).ncard = t.ncard - s.ncard` in a ring

  #19407 opened Nov 23, 2024

• chore: rename `CompleteLattice.Independent`/`.SetIndependent` to `iSupIndep`/`sSupIndep`

  #19409 opened Nov 23, 2024

• doc: describe why map_ofNat can't be simp (yet)

  #19410 opened Nov 23, 2024

• feat: `Polynomial.map f` strictly decreases the degree if `f p.leadingCoeff = 0`

  #19411 opened Nov 23, 2024

2 Issues closed by 2 people

• `to_additive` doesn't always translate proofs generated by simp

  #10830 closed Nov 20, 2024

• feat(Tactic/NormNum): add plugin for `Rat.num` and `Rat.den`

  #18826 closed Nov 19, 2024

4 Issues opened by 4 people

• Sharpness in linear_combination

  #19341 opened Nov 21, 2024

• Generalise Asymptotics API to drop commutative assumptions

  #19288 opened Nov 20, 2024

• Create a backbone of `Defs.lean` files

  #19253 opened Nov 19, 2024

• `lift` tries to clear variables even where they are still used

  #19160 opened Nov 17, 2024

185 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.

• refactor(Algebra/Category): turn homs in `AlgebraCat` into a structure

  #19065 commented on Nov 21, 2024 • 80 new comments

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

  #16160 commented on Nov 18, 2024 • 37 new comments

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

  #18486 commented on Nov 20, 2024 • 30 new comments

• feat: uniform time lemma for the existence of global integral curves

  #9013 commented on Nov 22, 2024 • 29 new comments

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

  #16675 commented on Nov 22, 2024 • 25 new comments

• feat(RingTheory): Jacobi-Zariski sequence

  #19067 commented on Nov 19, 2024 • 15 new comments

• fead: Add `lift_unique`, `lift_unique'` to `IsFractionRing`

  #19124 commented on Nov 23, 2024 • 14 new comments

• feat(RingTheory/LocalProperties): Add theorems about LocalizedModule

  #19080 commented on Nov 23, 2024 • 13 new comments

• feat(SetTheory/Ordinal/Veblen): the two-argument Veblen function

  #18611 commented on Nov 18, 2024 • 13 new comments

• feat: ring with discrete PrimeSpectrum

  #18891 commented on Nov 23, 2024 • 13 new comments

• feat: `Matrix.fromRows_one_isTotallyUnimodular_iff`

  #19076 commented on Nov 22, 2024 • 12 new comments

• feat: prove Dini's theorem for uniform convergence

  #19068 commented on Nov 20, 2024 • 11 new comments

• chore: change some `linarith`s to `linear_combination`s

  #18841 commented on Nov 22, 2024 • 9 new comments

• feat(GroupTheory/Subgroup/Centralizer): The `N/C` theorem

  #19006 commented on Nov 18, 2024 • 9 new comments

• feat(Algebra/Category): API for `Under R`

  #19058 commented on Nov 18, 2024 • 7 new comments

• refactor: turn `IsTorsionFree` into a typeclass

  #17672 commented on Nov 20, 2024 • 7 new comments

• feat(SetTheory/Ordinal/Nimber/Field): Nimber division

  #19066 commented on Nov 19, 2024 • 6 new comments

• feat(Data/List/SplitBy): characterization of `List.splitBy`

  #16837 commented on Nov 18, 2024 • 6 new comments

• feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and `mk`

  #18178 commented on Nov 17, 2024 • 5 new comments

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

  #16303 commented on Nov 19, 2024 • 5 new comments

• feat(Topology/EMetricSpace/Basic): add boundedness lemmas

  #18172 commented on Nov 21, 2024 • 5 new comments

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

  #17246 commented on Nov 17, 2024 • 5 new comments

• feat: the free locus of a (finitely presented) module

  #18691 commented on Nov 23, 2024 • 5 new comments

• feat(Order/InitialSeg): initial segments preserve successor limits

  #19053 commented on Nov 19, 2024 • 5 new comments

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

  #14866 commented on Nov 23, 2024 • 5 new comments

• feat: approximate units in C⋆-algebras

  #18506 commented on Nov 20, 2024 • 4 new comments

• feat(AlgebraicTopology/SimplicialSet): StrictSegal simplicial sets are 2-coskeletal

  #19057 commented on Nov 20, 2024 • 4 new comments

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

  #18578 commented on Nov 23, 2024 • 4 new comments

• feat(RingTheory/LocalProperties): flatness is a local property

  #19085 commented on Nov 23, 2024 • 4 new comments

• feat(Analysis/Complex): HasPrimitives on disc

  #9598 commented on Nov 18, 2024 • 4 new comments

• feat: `Countable` deriving handler

  #18557 commented on Nov 18, 2024 • 4 new comments

• feat(MeasureTheory/Measure/MutuallySingular): Disjoint iff mutually singular

  #17995 commented on Nov 18, 2024 • 3 new comments

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

  #18563 commented on Nov 18, 2024 • 3 new comments

• chore: move pointwise set files to `Algebra._.Pointwise`

  #19002 commented on Nov 23, 2024 • 3 new comments

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

  #16190 commented on Nov 22, 2024 • 3 new comments

• feat(GroupTheory/GroupAction/Primitive)

  #12052 commented on Nov 19, 2024 • 3 new comments

• feat(AlgebraicGeometry): the domain of definition of a rational map

  #18803 commented on Nov 23, 2024 • 3 new comments

• feat(Computability): regular languages are context-free

  #16311 commented on Nov 21, 2024 • 3 new comments

• feat: rewrite the linter for spaces before semicolons in Lean

  #16532 commented on Nov 23, 2024 • 3 new comments

• feat(SetTheory/Ordinal/CantorNormalForm): alternate CNF recursion principle

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

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

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

• [WIP] feat:Polynomial FLT

  #18882 commented on Nov 18, 2024 • 2 new comments

• feat(Algebra/Order/Monoid/Unbundled/WithTop): add lemmas about `WithTop.map` and `WithBot.map`

  #19122 commented on Nov 19, 2024 • 2 new comments

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

  #18534 commented on Nov 20, 2024 • 2 new comments

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

  #14411 commented on Nov 19, 2024 • 2 new comments

• refactor: allow `deriv` to be used on topological vector spaces

  #19108 commented on Nov 19, 2024 • 2 new comments

• feat(SetTheory/Ordinal/Clubs): define club sets and prove basic properties

  #14060 commented on Nov 18, 2024 • 2 new comments

• feat(CategoryTheory): command that generates instances for `MorphismProperty`

  #18785 commented on Nov 19, 2024 • 2 new comments

• feat(AlgebraicGeometry): covers of schemes over a base

  #19096 commented on Nov 18, 2024 • 2 new comments

• feat(AlgebraicGeometry): preimmersions are stable under base change

  #18915 commented on Nov 23, 2024 • 1 new comment

• feature(Algebra/Module/NestAlgebra): Nest algebras

  #18705 commented on Nov 22, 2024 • 1 new comment

• feat(AlgebraicTopology/HomotopyCat): SSet.hoFunctor

  #16783 commented on Nov 20, 2024 • 1 new comment

• feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas

  #18933 commented on Nov 21, 2024 • 1 new comment

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

  #18414 commented on Nov 17, 2024 • 1 new comment

• feat: orbits of an irrational rotation are dense

  #16596 commented on Nov 21, 2024 • 1 new comment

• feat: Lindemann-Weierstrass Theorem

  #6718 commented on Nov 23, 2024 • 1 new comment

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

  #17813 commented on Nov 23, 2024 • 1 new comment

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

  #18389 commented on Nov 17, 2024 • 1 new comment

• feat(Algebra/Star/Unitary): add unitarySubgroup

  #11820 commented on Nov 18, 2024 • 1 new comment

• feat: Hopf algebra structure on monoid algebras

  #13609 commented on Nov 18, 2024 • 1 new comment

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

  #18510 commented on Nov 19, 2024 • 1 new comment

• feat(Data/Nat): faster computation of Nat.log

  #17325 commented on Nov 18, 2024 • 1 new comment

• feat(Probability/Kernel): `Kernel.sectL` and `sectR`

  #15466 commented on Nov 21, 2024 • 1 new comment

• doc(Order/InitialSeg): Improve documentation

  #15874 commented on Nov 23, 2024 • 1 new comment

• feat(Combinatorics/SimpleGraph): Add definitions and theorems about the coloring of sum graphs

  #18677 commented on Nov 17, 2024 • 0 new comments

• feat: add theorems to transfer `IsGalois` between pairs of fraction rings

  #19125 commented on Nov 23, 2024 • 0 new comments

• feat: add leftmost derivation in context free grammar

  #18672 commented on Nov 21, 2024 • 0 new comments

• feat : define Artin braid groups

  #18626 commented on Nov 21, 2024 • 0 new comments

• feat: add `NonUnital{Star}Algebra.elemental` subalgebras

  #18615 commented on Nov 20, 2024 • 0 new comments

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

  #18580 commented on Nov 19, 2024 • 0 new comments

• feat: `Encodable` deriving handler

  #18564 commented on Nov 18, 2024 • 0 new comments

• feat(AlgebraicGeometry): the algebraic De Rham complex

  #18551 commented on Nov 22, 2024 • 0 new comments

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

  #18547 commented on Nov 17, 2024 • 0 new comments

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

  #18502 commented on Nov 18, 2024 • 0 new comments

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

  #18501 commented on Nov 16, 2024 • 0 new comments

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

  #18497 commented on Nov 23, 2024 • 0 new comments

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

  #18469 commented on Nov 19, 2024 • 0 new comments

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

  #18463 commented on Nov 20, 2024 • 0 new comments

• feat: stop `ring`/`abel` from seeing algebraic operations inside `let`s

  #19120 commented on Nov 21, 2024 • 0 new comments

• chore: allow Module over Semiring be Flat

  #19115 commented on Nov 20, 2024 • 0 new comments

• feat(CategoryTheory/Closed): functor categories are monoidal closed

  #19103 commented on Nov 17, 2024 • 0 new comments

• chore(Algebra.Polynomial): split `Polynomial/Basic.lean` into smaller files

  #19097 commented on Nov 20, 2024 • 0 new comments

• chore(Data/Finsupp): split off extensionality from `Defs.lean`

  #19092 commented on Nov 18, 2024 • 0 new comments

• chore(Algebra/MonoidAlgebra): split Defs.lean further

  #19091 commented on Nov 18, 2024 • 0 new comments

• chore(Data/Finsupp): split off material on `single`, `update`, `erase`

  #19087 commented on Nov 18, 2024 • 0 new comments

• feat(Topology/FiberBundle/Trivialization): local lifting through a Trivialization

  #19056 commented on Nov 16, 2024 • 0 new comments

• Test precompilation (batteries + aesop) again

  #19055 commented on Nov 18, 2024 • 0 new comments

• refactor(SetTheory/Ordinal/Arithmetic): redefine `IsLimit` to `IsSuccLimit`

  #19054 commented on Nov 20, 2024 • 0 new comments

• feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot and succ cases)

  #19047 commented on Nov 19, 2024 • 0 new comments

• feat: define class `SemigroupAction`

  #19046 commented on Nov 22, 2024 • 0 new comments

• feat: add option `pp.mathlib.binderPredicates`

  #19040 commented on Nov 19, 2024 • 0 new comments

• refactor(Probability.Martingale.BorelCantelli): move and simplify lemmas about indicators

  #19039 commented on Nov 22, 2024 • 0 new comments

• chore(Data/Set): split the `CoeSort` instance to its own file

  #19031 commented on Nov 18, 2024 • 0 new comments

• chore(Data/Set/Basic): remove redundant redeclarations

  #19023 commented on Nov 21, 2024 • 0 new comments

• feat(Algebra/BigOperators/Fin): Add `finSigmaFinEquiv`

  #19013 commented on Nov 18, 2024 • 0 new comments

• chore(Util/Superscript): use `register_parser_alias`

  #19009 commented on Nov 18, 2024 • 0 new comments

• feat: sup-closed sets are closed under finite suprema

  #18990 commented on Nov 16, 2024 • 0 new comments

• feat: relate lists and infinite sequences

  #18985 commented on Nov 18, 2024 • 0 new comments

• feat(CategoryTheory/Enriched): enrichement of functor categories over a functor category

  #18976 commented on Nov 17, 2024 • 0 new comments

• chore: generalize Module to NonUnitalSemiring

  #18969 commented on Nov 22, 2024 • 0 new comments

• chore: deprecate `Trunc`

  #18952 commented on Nov 17, 2024 • 0 new comments

• feat: add `mul_min` and `min_mul`

  #18926 commented on Nov 19, 2024 • 0 new comments

• feat(EReal): add `toENNReal`

  #18885 commented on Nov 20, 2024 • 0 new comments

• feat(Data/Nat/Nth): `nth_add_one`

  #18836 commented on Nov 23, 2024 • 0 new comments

• refactor: deprecate `MulEquivClass`

  #18806 commented on Nov 18, 2024 • 0 new comments

• feat (RingTheory/HahnSeries/Summable) add pointwise product operation

  #18794 commented on Nov 17, 2024 • 0 new comments

• feat(SetTheory/Cardinal/Arithmetic): omega ordinals are additively/multiplicatively principal

  #18778 commented on Nov 18, 2024 • 0 new comments

• feat(MeasureTheory/Integral/RieszMarkovKakutani) prove that the Riesz content is indeed a content for `NNReal`

  #18775 commented on Nov 19, 2024 • 0 new comments

• `to_additive` feature requests / issues

  #1074 commented on Nov 20, 2024 • 0 new comments

• chore: redefine `Nat.bit` `Nat.div2` `Nat.bodd`

  #13649 commented on Nov 22, 2024 • 0 new comments

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

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

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

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

• feat(CategoryTheory/Monoidal): redefine `Mon_` as a type class

  #15254 commented on Nov 16, 2024 • 0 new comments

• feat(CStarAlgebra): matrices with entries in a C⋆-algebra

  #15277 commented on Nov 17, 2024 • 0 new comments

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

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

• Lean pr testing 4938

  #15598 commented on Nov 19, 2024 • 0 new comments

• feat(RingTheory/MvPolynomial/Ideal): introduce new lemmas about MvPolynomial Ideals

  #15809 commented on Nov 18, 2024 • 0 new comments

• feat: greedy colorings of finite graphs

  #15822 commented on Nov 18, 2024 • 0 new comments

• feat: define singular `n`-manifolds

  #15906 commented on Nov 18, 2024 • 0 new comments

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

  #15915 commented on Nov 19, 2024 • 0 new comments

• feat: add `ProdQuotientMapSpace`

  #15943 commented on Nov 21, 2024 • 0 new comments

• feat(SetTheory/Ordinal/Principal): simplify characterization of additively principal ordinals

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

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

  #16020 commented on Nov 20, 2024 • 0 new comments

• Test/ci olean size

  #16062 commented on Nov 22, 2024 • 0 new comments

• Clean up quotient APIs

  #16210 commented on Nov 20, 2024 • 0 new comments

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

  #16314 commented on Nov 17, 2024 • 0 new comments

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

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

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

  #16361 commented on Nov 23, 2024 • 0 new comments

• Tactic wishlist

  #10361 commented on Nov 21, 2024 • 0 new comments

• A better notation for limit

  #16794 commented on Nov 22, 2024 • 0 new comments

• Linter for unused `variable` declarations

  #18720 commented on Nov 21, 2024 • 0 new comments

• feat/refactor: redefinition of homology + derived categories

  #4197 commented on Nov 18, 2024 • 0 new comments

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

  #5297 commented on Nov 20, 2024 • 0 new comments

• feat: more `PGame.identical` `PGame.memₗ` `PGame.memᵣ` APIs

  #5901 commented on Nov 18, 2024 • 0 new comments

• feat(LinearAlgebra/Matrix/SVD): Singular Value Decomposition of R or C Matrices

  #6042 commented on Nov 18, 2024 • 0 new comments

• feat(CategoryTheory/Sites): descent of sheaves

  #8661 commented on Nov 18, 2024 • 0 new comments

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

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

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

  #10235 commented on Nov 19, 2024 • 0 new comments

• feat(Topology/UniformSpace): define uniform preordered space

  #10476 commented on Nov 19, 2024 • 0 new comments

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

  #12048 commented on Nov 22, 2024 • 0 new comments

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

  #12053 commented on Nov 22, 2024 • 0 new comments

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

  #12405 commented on Nov 19, 2024 • 0 new comments

• feat(CategoryTheory): the localized category is monoidal

  #12728 commented on Nov 18, 2024 • 0 new comments

• Lean pr testing 4152

  #13079 commented on Nov 19, 2024 • 0 new comments

• Lean pr testing 4272

  #13191 commented on Nov 19, 2024 • 0 new comments

• feat: mabel tactic for multiplicative abelian groups

  #13442 commented on Nov 18, 2024 • 0 new comments

• Lean pr testing 4223

  #13646 commented on Nov 19, 2024 • 0 new comments

• WIP: Frobenius Elements

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

• feat: notation for Euclidean space

  #17732 commented on Nov 22, 2024 • 0 new comments

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

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

• feat(SetTheory/Ordinal/Veblen): epsilon and gamma ordinals

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

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

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

• refactor: introduce `Ideal.IsTwoSided` class for quotients of noncommutative rings

  #17930 commented on Nov 20, 2024 • 0 new comments

• doc: factorial notation docstring

  #18085 commented on Nov 18, 2024 • 0 new comments

• refactor: add a `ContinuousSqrt` class to conclude `StarOrderedRing C(α, R)`

  #18102 commented on Nov 19, 2024 • 0 new comments

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

  #18142 commented on Nov 20, 2024 • 0 new comments

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

  #18197 commented on Nov 19, 2024 • 0 new comments

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

  #18206 commented on Nov 20, 2024 • 0 new comments

• chore(SetTheory/Ordinal/Basic): deprecate results on `WellOrder`

  #18208 commented on Nov 20, 2024 • 0 new comments

• feat(SetTheory/Ordinal/Basic): notation `typeLT α = type (α := α) (· < ·)`

  #18235 commented on Nov 19, 2024 • 0 new comments

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

  #18238 commented on Nov 19, 2024 • 0 new comments

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

  #18396 commented on Nov 20, 2024 • 0 new comments

• refactor(LinearAlgebra/SesquilinearForm): Hermitian sesquilinear maps

  #18406 commented on Nov 23, 2024 • 0 new comments

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

  #18434 commented on Nov 18, 2024 • 0 new comments

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

  #18444 commented on Nov 20, 2024 • 0 new comments

• chore(Filter/Bases): split

  #18450 commented on Nov 17, 2024 • 0 new comments

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

  #16543 commented on Nov 19, 2024 • 0 new comments

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

  #16705 commented on Nov 18, 2024 • 0 new comments

• feat: define `(a : ENat) ^ (b : ENat)`

  #16810 commented on Nov 18, 2024 • 0 new comments

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

  #16992 commented on Nov 21, 2024 • 0 new comments

• feat(SetTheory/ZFC/Ordinal): Alternate characterizations of ordinals

  #17001 commented on Nov 21, 2024 • 0 new comments

• feat(SetTheory/ZFC/Ordinal): von Neumann hierarchy of sets

  #17027 commented on Nov 19, 2024 • 0 new comments

• feat(Data/EReal): Add results about `EReal`

  #17087 commented on Nov 20, 2024 • 0 new comments

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

  #17129 commented on Nov 22, 2024 • 0 new comments

• feat(Geometry/Manifold): manifolds are locally path-connected

  #17142 commented on Nov 20, 2024 • 0 new comments

• feat: update the `ContDiff` definition to integrate analytic functions in the hierarchy

  #17152 commented on Nov 22, 2024 • 0 new comments

• feat(RingTheory/Polynomial/Hilbert): the Hilbert polynomial in terms of a natural number `d` and a polynomial `p : ℤ[X]`

  #17334 commented on Nov 23, 2024 • 0 new comments

• feat(Algebra/Category/ModuleCat): pullback of presheaves of modules

  #17366 commented on Nov 19, 2024 • 0 new comments

• feat(Algebra/ModuleCat/Differentials/Presheaf): the presheaf of relative differentials

  #17469 commented on Nov 19, 2024 • 0 new comments

• feat(Algebra/Category/ModuleCat): pullback of sheaves of modules

  #17494 commented on Nov 19, 2024 • 0 new comments

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

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

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

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

• feat: add a script to check for PR title and labelling

  #17649 commented on Nov 19, 2024 • 0 new comments

• feat: Set to Function

  #17686 commented on Nov 18, 2024 • 0 new comments

• feat: the unusedVariableCommand linter

  #17715 commented on Nov 18, 2024 • 0 new comments