Changelog

chore: update Mathlib dependencies 2024-10-22 (#18035) …

chore(deps): dependabot updates (#18026) …

refactor: merge `ExpChar` and `CharP` API (#18023) …

feat: `‖aba⁻¹b⁻¹ - 1‖ ≤ C ‖a - 1‖ ‖b - 1‖` (#18027) …

feat(Analysis/SpecificLimits/Basic): add lemmas about limits of fractions (#16768) …

chore(Topology/Algebra/SeparationQuotient): split (#18011) …

feat: semisimple rings are Artinian (#17557) …

chore(Pointwise/Finset): move `MonoidWithZero` and `Ring` results out (#17999) …

feat: `‖a * b * c‖ ≤ ‖a‖ * ‖b‖ * ‖c‖` (#18005) …

feat(AlgebraicGeometry): dominant morphisms of schemes (#17961)

RFC chore(GroupTheory/MonoidLocalization): un-`@[simp]` `Localization.mk_eq_monoidOf_mk'` (#18015) …

feat: add missing instances for `ContinuousMap` and `BoundedContinuousFunction` (#17838)

chore(CategoryTheory/Adjunction): homEquiv_unit is no longer a global simp lemma (#17761) …

chore: add dependabot (#18013) …

feat(Data/Real/IsNonarchimedean): add lemmas (#16767) …

feat: `a ^ n = 1 ↔ n = 0` and similar (#17745) …

feat(Module/ZLattice): define the pullback of a ZLattice (#16822) …

feat: Popoviciu's inequality (#17868) …

chore: remove `CoeFun` instances where `FunLike` is available (#17917) …

chore: add test to keep powering in `ZMod` fast (#17996) …

chore: removed unused variables (#17975) …

docs(Computability/EpsilonNFA): typo (#17992) …

feat(Topology/Inseparable): add `alias Specializes.of_eq := specializes_of_eq` (#17988) …

chore(Filter/Tendsto): split from `Basic` (#17959)

chore(RingTheory/DedekindDomain/FiniteAdeleRing): remove TODO (#17951) …

chore(Data/NNReal): split into `Defs` and `Basic` (#17913) …

feat(GroupTheory/Index): index of product of subgroups (#17878) …

feat(NumberTheory/Ostrowski): Ostrowski's Theorem for the rationals (#17138) …

chore: fix some nits from #12339 (#17994)

chore: cleanup adaptation notes from 2024-09-06 (#17990)

feat(ENNReal): liminf/limsup/iInf/iSup and multiplication (#17656) …

feat: the pi sigma-algebra is generated by projections (#17828) …

chore(ConditionalProbability): review argument implicitness (#17910) …

refactor(SetTheory/Ordinal/Arithmetic): deprecate `blsub₂` (#17679) …

feat: the multiGoal linter (#12339) …

chore: move batteries back to main; bump (#17991) …

chore: rename List.modifyNth->modify and insertNth->insertIdx (#17985) …

chore(build.in): update version of `gh-get-current-pr` action (#17978) …

feat(Data/Nat/Bitwise): add simp lemmas (#17977) …

feat(Data/Set/Basic): add `diff_insert_of_not_mem` (#17973) …

chore: more fixes for multigoal linter (#17966) …

chore: move `mul_ite`, add `dite` version, multiplicativise `ite_add_ite` (#17963)

feat: `negOnePow n = (-1 : ℤ) ^ n` (#17967) …

feat(CategoryTheory): natural version of `FullyFaithful.homEquiv` (#17450)

feat(Analysis/Normed/Field/Ultra): nonarchimedean iff norm of nats le one (#15077)

chore(Topology/Exterior): golf (#17955) …

chore(LinearAlgebra/TensorProduct): fix duplication (#17912) …

feat(CategoryTheory): pull colimits out of hom functors with Yoneda on the LHS (#17440) …

chore: Rename `ClosedEmbedding` to `IsClosedEmbedding` (#17937) …

feat(Analysis/Complex/Positivity): new file (#17862) …