Changelog

feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (#18087) …

feat(combinatorics/simple_graph): More clique lemmas (#19203) …

feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (#16976) …

move old README.md to OLD_README.md

doc: Add a warning mentioning Lean 4 to the readme (#19243) …

feat(topology/metric_space): diameter of pointwise zero and addition (#19028)

feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (#18629) …

feat(probability/independence): Independence of singletons (#18506) …

feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (#18612) …

feat(data/finset/lattice): `sup'`/`inf'` lemmas (#18989) …

chore(order/liminf_limsup): Generalise and move lemmas (#18628) …

feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (#17926)

feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (#11352) …

feat(analysis/convex/proj_Icc): Extending convex functions (#18797) …

feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (#17925)

feat(measure_theory/measure/haar_quotient): the Unfolding Trick (#18863) …

feat(linear_algebra/orientation): add `orientation.reindex` (#19236)

feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (#17828)

feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (#15260)

feat(tactic/positivity): Extension for `ite` (#17650) …

feat(analysis/normed_space/continuous_linear_map): generalize typeclass assumptions (#19108)

feat(linear_algebra/quadratic_form): some work from 'Clifford Algebras and Spinor Norms Over a Commutative Ring' (#18447)

feat(algebraic_topology/dold_kan): tools for compatibilities, lemmas (#17923)

feat(order/upper_lower/basic): Linear order (#19068) …

fix(group_theory/subgroup/basic): generalize `centralizer` from `subgroup G` to `set G` (#18965) …

docs(topology/dense_embedding): Improve explanation (#18134) …

chore(ring_theory/kaehler): cleanup instances (#19234) …

feat(ring_theory/tensor_product): add missing scalar tower instances (#19143)

feat(topology/metric_space/basic): decomposition of a "sphere" hypercube (#18875) …

chore(*): add mathlib4 synchronization comments (#19239) …

chore(set_theory/ordinal/basic): golf (#18547)

feat(order/irreducible): Sup-irreducible elements (#18999) …

chore(*): add mathlib4 synchronization comments (#19238) …

fix: handle archive and counterexamples correctly when adding port comments (#19237)

fix(tactic/linarith): instantiate metavariables in linarith (#19233) …

feat(set_theory/ordinal/natural_ops): define natural multiplication (#14324)

chore(*): add mathlib4 synchronization comments (#19231) …

fix(tactic/norm_num): Do not allow typos in simp lemmas if they are unused (#17981) …

feat(data/matrix/auto): lemmas for arbitrary concrete matrices generated via auto_params (#15738) …

feat(data/*/interval): `finset.uIcc` on concrete structures (#18838) …

feat(order/well_founded_set): `prod.lex` is well-founded (#18665)

feat(group_theory/order_of_element): Order in `α × β` (#18719) …

feat(analysis/calculus/fderiv/mul): derivative of inverse in division rings (#19127)

feat(*/prod): `prod_prod_prod` equivs (#19235) …

feat(analysis/inner_product_space/of_norm): Create an inner product from a norm (#4798) …

fix(control/traversable/derive): the `functor` deriving handler makes weird definitions for inductive types which have recursive arguments separated by a non-recursive argument (#19228) …

feat(analysis/normed/group/basic): norm lemmas for lipschitz and antilipschitz (#19103) …

fix(tactic/interval_cases): instantiate metavars (#19232) …

feat(data/list/dedup): Lemmas about `list.dedup` (#19142) …

feat(analysis/convex): convexity of n-ary sums (#18943)