Pull Requests leanprover-community/mathlib3

feat(topology/uniform_space/uniform_convergence_topology): `𝔖`-convergence depends only on the bornology generated by `𝔖` delegated t-topology modifies-synchronized-file too-late

#18009 opened 2022-12-24 15:38 by ADedecker

feat(combinatorics/simple_graph/chromatic): chromatic polynomial and that its evaluation computes cardinality of colorings WIP too-late

#18003 opened 2022-12-22 18:54 by kmill

feat(topology/uniform_space/ascoli): general Arzela-Ascoli theorem WIP t-topology t-analysis too-late

#17975 opened 2022-12-18 14:14 by ADedecker

fix(tactic/tauto) fix some bugs in symm_eq awaiting-review t-meta too-late

#17958 opened 2022-12-15 13:58 by dwrensha

feat(tactic/lift): prevent `lift` from failing if goal contains the hypothesis used to `lift` awaiting-author too-late

#17869 opened 2022-12-08 23:29 by adomani

feat(analysis/normed/ring/seminorm): Proof of equivalent definitions of nonarchimedean property WIP blocked-by-other-PR too-late

#17863 opened 2022-12-08 16:49 by Biiiilly

feat(ring_theory/mv_polynomial/homogeneous): refactor using weighted_homogeneous awaiting-author too-late

#17856 opened 2022-12-08 13:11 by mariainesdff

chore(data/set/basic): Split WIP awaiting-author merge-conflict awaiting-CI too-late

#17835 opened 2022-12-06 22:34 by Ruben-VandeVelde

feat(analysis/normed/ring/seminorm): add `equiv` and nonarchimedean property awaiting-author too-late

#17817 opened 2022-12-04 22:36 by Biiiilly

chore(data/set/pointwise/*): Resplit awaiting-author t-algebra too-late

#17812 opened 2022-12-04 12:59 by YaelDillies

refactor(analysis/calculus/fderiv): use right actions instead of .smul_right for multiplication WIP RFC too-late

#17802 opened 2022-12-03 01:10 by eric-wieser

feat(data/list/off_diag): add `list.off_diag` WIP too-late

#17769 opened 2022-11-30 09:20 by eric-wieser

feat(combinatorics/simple_graph/connectivity): number of connected components when deleting edges awaiting-review t-combinatorics too-late

#17654 opened 2022-11-21 00:30 by tjeremie

feat(ring_theory/integral_domain): generalize `card_fiber_eq_of_mem_range` awaiting-author t-algebra modifies-synchronized-file too-late

#17653 opened 2022-11-20 20:51 by urkud

feat(topology/metric_space/thickened_indicator): Add convergence of plain old indicators of thickenings. awaiting-author t-topology too-late

#17648 opened 2022-11-20 15:03 by kkytola

refactor(*): assume `≠0` instead of `0 < _` awaiting-author t-algebra too-late

#17612 opened 2022-11-18 22:40 by urkud

feat(linear_algebra/matrix_group): introduce ```matrix_group``` and instances awaiting-author undergrad t-algebra too-late

#17608 opened 2022-11-18 14:48 by vasnesterov

feat(archive/bell_inequality): Bell's 1964 inequality awaiting-review t-measure-probability not-too-late

#17570 opened 2022-11-16 16:37 by ianjauslin-rutgers

feat(algebraic_geometry/morphisms/affine): Define affine morphisms awaiting-author t-algebraic-geometry too-late

#17560 opened 2022-11-16 06:59 by erdOne

feat(topology/sheaves/stalks): Generalize to `stalk_pushforward_iso_of_inducing` awaiting-author t-topology t-algebraic-geometry too-late

#17539 opened 2022-11-14 13:23 by erdOne

feat(ring_theory/local_properties): Being (in/sur/bi)jective is local (for linear maps). awaiting-author t-algebra too-late

#17472 opened 2022-11-11 07:30 by erdOne

feat(analysis/locally_convex/with_seminorms): equicontinuity criterions WIP t-analysis modifies-synchronized-file too-late

#17275 opened 2022-10-30 21:40 by ADedecker

feat(topology/continuous_on): add `tendsto_nhds_within_iff_seq_tendsto` awaiting-author t-topology too-late

#17261 opened 2022-10-30 13:50 by RemyDegenne

feat(data/finsupp): generalise support in finsupp awaiting-author merge-conflict awaiting-CI too-late

#17211 opened 2022-10-27 16:16 by zeramorphic

feat(data/int/gcd): Extended gcds involving 1 modifies-synchronized-file too-late

#17201 opened 2022-10-27 05:12 by tb65536

feat(ring_theory/derivation): The differential module under base change. ready-to-merge delegated awaiting-CI t-algebra too-late

#17198 opened 2022-10-26 19:47 by erdOne

feat(topology/inseparable): Define `specializing` maps between topological spaces awaiting-author t-topology too-late

#17113 opened 2022-10-22 17:11 by erdOne

feat(category_theory/groupoid/quotient): quotients and presentations of groupoids needs-refactor merge-conflict t-algebra too-late

#17109 opened 2022-10-22 06:25 by bottine

feat(number_theory/divisors): add divisors_mul awaiting-author t-number-theory too-late

#17041 opened 2022-10-18 09:13 by eric-wieser

feat(measure_theory/integral/riesz_markov_kakutani): Finish construction of content for Riesz-Markov-Kakutani awaiting-author t-analysis too-late

#17027 opened 2022-10-17 01:53 by ReimannJ