Changelog

chore: import `Tactic.Positivity.Finset` in `Tactic.Positivity` (#18146) …

chore: nolint `div_le_div_iff'` (#19309) …

chore: reducibility in gcongr apply step (#19262) …

feat(Order/Max): add `IsTop.isMax_iff` and `IsBot.isMin_iff` (#19305) …

fix: more explicit PR number in `bors x` actions (#19304)

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

feat(Topology/MetricSpace/Pseudo/Defs): add `dense_iff_iUnion_ball` and `dist_eq_of_dist_zero` (#19294) …

feat(AlgebraicGeometry): Proj is separated (#19290) …

fix: `>>` and print author (#19300) …

chore(RingTheory): improve and generalize submodule localization API (#19118) …

feat(NumberTheory/LSeries/DirichletContinuation): results on logarithmic derivatives (#19254) …

chore(CategoryTheory/IsConnected): add refl etc annotations (#19017)

feat(CI): merge bors (#19078) …

fix(CI): fail if tests are noisy (#19268) …

feat: the Lie bracket of vector fields in vector spaces (#18852)

chore: deprecate `Quotient.out'` (#17941)

feat(UpperHalfPlane): weaken assumptions of multiple atImInfty lemmas (#16015) …

feat(KrullDimension): height refactor module docstring (#15524) …

feat(CI): add a log of the size of the oleans (#19283) …

feat: change definition of `HasFTaylorSeries` to take a parameter in `WithTop ℕ∞` instead of `ℕ∞` (#18723) …

ci: print the existing update PR, if found (#19218) …

feat: expand API around manifold derivatives (#18850) …

feat: the monoidal category structure on homological complexes (#15695) …

feat: cardinality of `Field.Emb` for algebraic extensions of infinite separable degree (#9480) …

feat(KrullDimension): concrete calculations (#19210) …

chore: bump dependencies (#19279)

chore(RingTheory): split `UniqueFactorizationDomain.lean` (#19256) …

feat: `Nat.cast_nonpos` (#19247) …

feat: `IsScalarTower` and `SMulCommClass` instances for pointwise actions of submodules (#19214) …

chore(discover-lean-pr-testing): properly fetch tags (#19204) …

chore: deprecate `LinearOrderedCommGroupWithZero` lemmas (#19197) …

feat: bounds for modular forms of non-positive weights (#18192) …

feat(ModelTheory): Ax-Grothendieck (#6468)

chore(Algebra/Module): further split `Defs.lean` (#18995) …

chore: delete unused private lemma in Complex/exponential (#19263)

chore: no `open Foo` after `namespace Foo` (#19223) …

feat(Order/WithBot): Equiv.withBotSubtypeNe (#19251) …

refactor(EReal): add add/sub lemmas and refactor limsup_add on EReal (#18879) …

feat(Data/Nat/Nth): `nth_mem_anti` (#19169) …

feat: `maintainer merge?`/`maintainer delegate?` switch for spoiler (#19230)

feat: commutativity of `NonUnital{Star}Algebra.adjoin` (#18612)

feat: `#parse` -- a command to parse text and log outputs (#16305) …

feat(SetTheory/ZFC/Ordinal): Initial development of ordinals in ZFSet (#15793) …

chore: generalise `div_le_div` to groups with zero (#18917) …

chore: make `Finset.subset_union_left` simp (#19249) …

fix: assert_not_exists `CStarRing` that exists but not here (#19226) …

feat: `IsSelfAdjoint.smul_iff` (#19216) …

feat: quantales (#17289) …

feat: `norm_num` extension for `Rat.num` and `Rat.den` (#19099) …

feat: define instances of `Finite`, `Fintype`, `DecidableEq` for `MulEquiv` (#17057)