Changelog

refactor(*/Multilinear): change `*.ofSubsingleton` (#8694) …

feat: Add `Polynomial.separable_map'`. (#8680)

feat: composition of a multilinear map and linear maps is multilinear (#8687)

feat: multilinearity of the `MultilinearMap.compLinearMap` operation (#8684)

feat(Topology/GDelta): rename "nowhereDense" to "isNowhereDense" (#8567) …

fix: CI badge appears twice in readme (#8689)

feat(CategoryTheory/Sites): internal hom of (pre)sheaves (#8622) …

feat(FieldTheory/SeparableDegree): basic definition of separable degree of field extension (#8117) …

refactor: use the new homology API for right derived functors (#8593) …

feat(CategoryTheory): the localized category of a product category (#8516) …

feat(CategoryTheory): naturality of the connecting homomorphism of the snake lemma (#8490) …

feat: weights of Lie modules are linear functions (#8677) …

feat: Relax arguments of going-up theorems. (#8645)

feat: `IsFractionRing R R` if `R` is a field. (#8641)

feat: Add lemmas about `Polynomial.scaleRoots`. (#8653)

feat: Add `IsAlgebraic.inv_iff`. (#8651)

feat: add some results about IsCyclic (#8625) …

refactor(Probability/Density): define pdf using rnDeriv (#8544) …

feat: computation of the connecting homomorphism of the snake lemma in concrete categories (#8512) …

chore: bump dependencies (#8671)

chore: build lean4checker with current toolchain (#8669) …

chore: bump for std4#241 (#6975) …

Update docstring of `squeeze_one_norm'` (#8667) …

fix(Cache): correctly handle local copies of `Mathlib` (#8662) …

feat: a family of generalized eigenvalues for a commuting linear family of endomorphims must be linear (#8656)

feat: bounds for Dirichlet characters (#8449) …

feat: Add `AlgHom.map_adjoin_singleton`. (#8655)

feat: Add `Submodule.restrictScalars_mul`. (#8649)

feat: Add `not_isNilpotent_one`. (#8648)

feat(Data/Set/Lattice): generalize `Set.iUnion_univ_pi` (#8647) …

feat(Topology/Bornology): add convenience lemmas (#8640) …

feat: remove an assumption (#8646) …

feat(SpecialFunctions/Log): add `tendsto_log_nhdsWithin_zero_right` (#8554) …

feat(LinearAlgebra/TensorProduct): add `liftAddHom` (#8584) …

chore: update the nightly-with-mathlib branch at leanprover/lean4 (#8628) …

chore: merge master into nightly-testing via cron, not on every commit (#8627) …

chore: `ValuedCsp` and `ValuedCsp.Instance` changed from `def` to `abbrev` (#8623)

feat(Data/Finset/Card): add converse to some existing theorems (#8515) …

refactor(Data/Matrix/Basic): use a defeq for scalar that matches its docstring (#8115) …

chore(GroupTheory/Congruence): small cleanups (#8314) …

chore: add docs + alias for `prod_bijective` (#8439)

chore: implement simp_rw config matching better (#8592)

chore: bump dependencies (#8626)

fix: patch for std4#203 (more sub lemmas for `Nat`) (#6216)

chore: delete `LinearMap.extendScalars` which duplicates `LinearMap.baseChange` (#8617) …

doc(Computability/Halting): Mark named theorems (#8577) …

feat: prove an upper bound on bitwise operations (#8598) …

doc: add a better docstring for `fun₀` (#8601)

chore: Fix universe (misprint in Portmanteau.lean). (#8620) …

feat(AlgebraicGeometry): the big Zariski site (#8549) …