Pull Requests leanprover-community/mathlib3

feat(data/finsupp/basic): Lemmas regarding `finsupp.filter` awaiting-review modifies-synchronized-file too-late

#17012 opened 2022-10-16 08:17 by erdOne

feat(src/ring_theory/is_tensor_product): Base change along a surjection. awaiting-review t-algebra modifies-synchronized-file too-late

#17010 opened 2022-10-16 07:32 by erdOne

feat(category_theory/*): Monoid objects in Abelian group are rings WIP awaiting-CI t-algebra too-late

#17006 opened 2022-10-16 02:27 by jjaassoonn

refactor(number_theory/divisors): redefine nat.divisors as a monoid hom awaiting-author awaiting-CI too-late

#16917 opened 2022-10-11 19:27 by b-mehta

feat(topology/sheaves/Godement): define the first term of Godement resolution awaiting-review awaiting-CI t-algebraic-geometry too-late

#16878 opened 2022-10-09 05:01 by jjaassoonn

feat(tactic/recommend): `recommend` tactic based on premise selection t-meta modifies-tactic-syntax not-too-late

#16807 opened 2022-10-04 23:19 by gebner

feat(information_theory/linear_code): Define linear codes WIP awaiting-CI too-late

#16774 opened 2022-10-03 04:39 by BoltonBailey

feat (group_theory/amenable) : Finite groups are amenable awaiting-review blocked-by-other-PR too-late

#16695 opened 2022-09-29 07:15 by matthias567

feat(analysis/locally_convex/barrel): barreled spaces WIP modifies-synchronized-file too-late

#16681 opened 2022-09-28 08:57 by ADedecker

chore(data/real/nnreal): make `real.to_nnreal` computable awaiting-review too-late

#16645 opened 2022-09-25 21:04 by eric-wieser

feat(algebraic_topology/fundamental_groupoid): Add topological retraction and relate to category_theory retraction awaiting-author t-topology too-late

#16615 opened 2022-09-23 20:53 by mlavrent

feat (group_theory/amenable) : Folner sequences, Folner amenability, example integers awaiting-review blocked-by-other-PR too-late

#16581 opened 2022-09-21 12:33 by matthias567

feat (group_theory/amenable): Free groups are not amenable awaiting-review blocked-by-other-PR too-late

#16580 opened 2022-09-21 12:25 by matthias567

feat (group_theory/amenable) : Extensions of Amenable groups are amenable awaiting-review blocked-by-other-PR too-late

#16578 opened 2022-09-21 12:16 by matthias567

feat (group_theory/amenable) : Subgroups of Amenable Groups are Amenable awaiting-review blocked-by-other-PR too-late

#16576 opened 2022-09-21 12:09 by matthias567

feat (group_theory/amenable) : Quotients of amenable groups are amenable awaiting-review blocked-by-other-PR too-late

#16575 opened 2022-09-21 12:04 by matthias567

feat (group_theory/amenable) : define amenable groups awaiting-review too-late

#16574 opened 2022-09-21 11:28 by matthias567

feat(data/list/rotate): rotate right WIP too-late

#16538 opened 2022-09-17 21:17 by BoltonBailey

feat(analysis/normed/ring/seminorm_constructions): add seminorm_from_const WIP t-analysis too-late

#16526 opened 2022-09-16 11:58 by mariainesdff

feat(analysis/inner_product_space/cross_product): general construction of the cross-product awaiting-author t-algebra too-late

#16490 opened 2022-09-12 22:11 by hrmacbeth

feat(algebra/order/monoid_lemma_zero_lt): change tracking t-algebra t-order too-late

#16449 opened 2022-09-09 19:17 by astrainfinita

Reimplement primrec based on trees WIP blocked-by-other-PR too-late

#16416 opened 2022-09-07 17:58 by prakol16

feat(logic/encodable): Encoding of elements as trees awaiting-review too-late

#16415 opened 2022-09-07 16:44 by prakol16

feat(analysis/inner_product_space/reproducing_kernel): Reproducing kernel Hilbert spaces awaiting-author t-analysis too-late

#16351 opened 2022-09-02 13:36 by shingtaklam1324

feat(data/nat/factorization/basic): lemmas about factorizations of sums and subtractions awaiting-author too-late

#16231 opened 2022-08-24 10:44 by stuart-presnell

refactor(data/dfinsupp/basic): move material on `dfinsupp.sum` and `dfinsupp.prod` to new file awaiting-author too-late

#16174 opened 2022-08-20 20:14 by stuart-presnell

feat(data/{sum/order, prod/lex}): `is_well_founded` and `is_well_order` instances awaiting-review awaiting-CI t-order too-late

#16140 opened 2022-08-18 23:08 by vihdzp

feat(combinatorics/graph/multi/basic): Indexed multigraphs awaiting-author t-combinatorics too-late

#16100 opened 2022-08-17 13:49 by YaelDillies

feat(linear_algebra/clifford_algebra/spin_group) : Spin Group WIP too-late

#16040 opened 2022-08-13 15:02 by Biiiilly

refactor(set_theory/ordinal/cantor_normal_form): CNF as an association list awaiting-review merge-conflict modifies-synchronized-file not-too-late

#16010 opened 2022-08-11 15:37 by vihdzp