Pull Requests leanprover-community/mathlib3

chore(*): add mathlib4 synchronization comments easy awaiting-review mathlib4-synchronization

#19240 opened 2023-08-20 00:19 by github-actions[bot]

feat(topology/algebra/infinite_sum) : define infinite products awaiting-review modifies-synchronized-file too-late

#19219 opened 2023-06-29 14:02 by AntoineChambert-Loir

Test leanprover-community/lean#812 WIP too-late

#19192 opened 2023-06-15 10:28 by eric-wieser

feat(measure_theory/measure): show that bounded continuous functions separate measures too-late

#19189 opened 2023-06-14 12:52 by pfaffelh

feat(topology/algebra/infinite_sum): Extract `none` from a sum over `option` types awaiting-author modifies-synchronized-file too-late

#19150 opened 2023-06-04 00:00 by dtumad

feat(analysis/calculus/fderiv/exp): derivative of `exp ℝ (A x)` in non-commutative rings help-wanted WIP too-late

#19056 opened 2023-05-21 23:37 by eric-wieser

refactor(measure_theory/measure/lebesgue): use `‖a‖₊ •` instead of `ennreal.of_real (|a|) *` WIP awaiting-CI modifies-synchronized-file too-late

#19018 opened 2023-05-15 12:28 by eric-wieser

feat(measure_theory/measure/haar_lebesgue): the volume measures on `euclidean_space ℝ ι` and `ι → ℝ` agree WIP t-measure-probability modifies-synchronized-file too-late

#19013 opened 2023-05-14 22:35 by eric-wieser

feat(library): max-flow min-cut help-wanted WIP too-late

#18998 opened 2023-05-12 11:10 by amilchew

feat(library): weak duality of max-flow min-cut theorem awaiting-review too-late

#18996 opened 2023-05-12 10:41 by amilchew

refactor(linear_algebra/*): Rename `linear_equiv.range` to `linear_equiv.range_eq_top` WIP awaiting-CI modifies-synchronized-file too-late

#18969 opened 2023-05-08 12:36 by tb65536

feat(order/filter,topology/instances/nnreal): upgrade some lemmas to `iff` awaiting-author t-topology t-order modifies-synchronized-file too-late

#18964 opened 2023-05-07 19:42 by urkud

feat(zmod/basic) modifies-synchronized-file too-late

#18953 opened 2023-05-06 09:24 by laughinggas

feat(ring_theory/derivation): support non-commutative rings (via bimodules) WIP too-late

#18936 opened 2023-05-03 23:16 by eric-wieser

refactor(number_theory/modular_forms/slash_actions): slash actions are families of `distrib_mul_action`s RFC t-number-theory too-late

#18932 opened 2023-05-03 14:16 by eric-wieser

feat(algebra/*): morphisms from closures are equal if they agree on generators awaiting-review awaiting-CI t-algebra modifies-synchronized-file too-late

#18836 opened 2023-04-19 15:52 by eric-wieser

feat(inner_product_space/positive): matrix.pos_semidef iff x.to_euclidean_lin.is_positive awaiting-review blocked-by-other-PR not-too-late

#18786 opened 2023-04-10 09:46 by themathqueen

feat(inner_product_space/positive): defines square root of a linear map blocked-by-other-PR not-ready-to-merge t-analysis

#18779 opened 2023-04-09 13:24 by themathqueen

feat(topology/noetherian_space): use `well_founded_(lt/gt)` awaiting-review too-late

#18776 opened 2023-04-09 02:13 by vihdzp

chore(*): bundle typeclasses awaiting-review awaiting-CI t-order too-late

#18775 opened 2023-04-09 01:23 by vihdzp

chore(data/fintype/card): instance `well_founded_of_trans_of_irrefl` awaiting-review awaiting-CI modifies-synchronized-file too-late

#18774 opened 2023-04-09 01:09 by vihdzp

chore(logic/hydra): instance `well_founded.cut_expand` awaiting-author modifies-synchronized-file too-late

#18757 opened 2023-04-07 16:15 by vihdzp

feat(order/well_founded): `well_founded_lt.has_min`, etc. awaiting-review blocked-by-other-PR too-late

#18751 opened 2023-04-06 18:34 by vihdzp

feat(order/rel_classes): housekeeping awaiting-review blocked-by-other-PR t-order modifies-synchronized-file not-too-late

#18750 opened 2023-04-06 17:50 by vihdzp

feat(logic/relation): auxiliary `forall_exists_rel` relation awaiting-author modifies-synchronized-file too-late

#18713 opened 2023-04-02 02:24 by vihdzp

feat(set_theory/game/ordinal): API for casting ordinals into games awaiting-author too-late

#18703 opened 2023-03-30 09:36 by vihdzp

refactor(order/rel_classes): remove redundant hypothesis from `is_well_order` awaiting-review t-order modifies-synchronized-file not-too-late

#18702 opened 2023-03-30 09:01 by vihdzp

feat(combinatorics.quiver): Schreier and Cayley graphs WIP blocked-by-other-PR t-algebra t-combinatorics not-too-late

#18693 opened 2023-03-29 12:46 by bottine

feat(combinatorics.simple_graph.metric): `enat` valued dist function on graphs WIP t-topology t-combinatorics too-late

#18692 opened 2023-03-29 12:39 by bottine

feat(combinatorics.simple_graph.acyclic): Trees are maximal acyclic, resp. minimal connected graphs. WIP t-combinatorics too-late

#18685 opened 2023-03-28 16:04 by bottine