Pull Requests leanprover-community/mathlib3

feat(combinatorics.simple_graph.ends): A version of Freudenthal-Hopf WIP blocked-by-other-PR t-combinatorics too-late

#18681 opened 2023-03-28 07:37 by bottine

feat(ring_theory/polynomial/vieta): add some variations on `prod_X_sub_C_coeff` awaiting-author awaiting-CI too-late

#18641 opened 2023-03-23 20:10 by Xialu3421

feat(ring_theory/mv_polynomial/symmetric): sum of symmetric polynomials is symmetric awaiting-author too-late

#18640 opened 2023-03-23 20:01 by Xialu3421

refactor(data/list/nat_antidiagonal): extend to `enat` WIP too-late

#18581 opened 2023-03-14 14:40 by eric-wieser

feat(nat/basic): Properties of natural numbers awaiting-author modifies-synchronized-file too-late

#18570 opened 2023-03-11 14:04 by laughinggas

feat(set_theory/zfc/ordinal): von Neumann hierarchy awaiting-review not-too-late

#18521 opened 2023-03-01 08:37 by vihdzp

refactor(set_theory/game/*): remove `relabelling` WIP too-late

#18518 opened 2023-03-01 04:05 by astrainfinita

feat(set_theory/zfc/ordinal): definition of von Neumann ordinals awaiting-review not-too-late

#18513 opened 2023-02-28 13:40 by vihdzp

feat(combinatorics/quiver): isomorphisms of quivers delegated t-combinatorics modifies-synchronized-file not-too-late

#18511 opened 2023-02-28 07:56 by bottine

refactor(analysis/normed/group/basic): unbundle algebra from norm structure WIP RFC t-analysis too-late

#18462 opened 2023-02-17 21:06 by eric-wieser

refactor(computability/language): unify with set_semiring awaiting-CI too-late

#18451 opened 2023-02-16 00:36 by eric-wieser

feat(order/rel_iso/basic): add `rel_covering`, main defs only awaiting-author merge-conflict t-order modifies-synchronized-file too-late

#18418 opened 2023-02-10 06:48 by astrainfinita

feat(topology/metric_space/path_metric): Definition of the path metric on a metric space and proof of its idempotency awaiting-author t-topology too-late

#18375 opened 2023-02-03 17:02 by bottine

chore(*): Improve simp confluence on `foo_equiv.symm` help-wanted WIP too-late

#18343 opened 2023-02-01 10:07 by YaelDillies

chore(set_theory/zfc/ordinal): rename `Set.is_transitive` to `Set.transitive` RFC awaiting-author too-late

#18339 opened 2023-01-31 13:50 by astrainfinita

feat(data/dfinsupp/basic): remove decidable typeclass assumptions on `sigma_uncurry` awaiting-review too-late

#18318 opened 2023-01-27 17:03 by astrainfinita

feat(number_theory/bernoulli_polynomials): prove `bernoulli_eval_one_neg` awaiting-author t-number-theory too-late

#18313 opened 2023-01-26 23:37 by grhkm21

feat(set_theory/zfc/basic): even more lemmas not-ready-to-merge too-late

#18311 opened 2023-01-26 22:36 by vihdzp

feat(analysis/von_neumann_algebra/basic): one result awaiting-review blocked-by-other-PR t-analysis not-too-late

#18290 opened 2023-01-25 11:08 by themathqueen

feat(linear_algebra/invariant_submodule): invariant submodules awaiting-review t-algebra modifies-synchronized-file not-too-late

#18289 opened 2023-01-25 10:18 by themathqueen

refactor(data/finsupp): add decidable arguments everywhere WIP too-late

#18274 opened 2023-01-24 10:53 by eric-wieser

chore(order/filter/n_ary): redefine, golf awaiting-author t-topology t-order too-late

#18258 opened 2023-01-22 16:33 by urkud

feat(data/polynomial/partial_fractions): Uniqueness of Partial Fraction Decomposition WIP too-late

#18235 opened 2023-01-19 20:26 by thefundamentaltheor3m

feat(analysis/inner_product_space/positive): Positivity of linear maps not-ready-to-merge t-analysis

#18230 opened 2023-01-19 16:35 by themathqueen

feat(geometry/euclidean/congruence): define congruences awaiting-author awaiting-CI too-late

#18214 opened 2023-01-18 15:17 by JovanGerb

feat(category_theory): Internal categories help-wanted WIP too-late

#18204 opened 2023-01-18 03:45 by z-murray

feat(proj construction) too-late

#18138 opened 2023-01-11 23:55 by jjaassoonn

feat(order/rel_iso/basic): add `rel_covering`, golf awaiting-review blocked-by-other-PR t-order not-too-late

#18128 opened 2023-01-11 11:08 by astrainfinita

feat(analysis/inner_product_space/finite_dimensional): some lemmas on finite dimensional inner product spaces awaiting-review blocked-by-other-PR t-analysis not-too-late

#18041 opened 2023-01-02 15:03 by themathqueen

feat(topology/uniform_space/uniform_convergence_topology): prove completeness WIP too-late

#18017 opened 2022-12-26 23:43 by ADedecker