leanprover-community/mathlib

Pull Requests Commits

Jon Eugster committed 3 years ago

eac8edde

chore(scripts): update nolints.txt (#17425)

leanprover-community-bot committed 3 years ago

f520632b

feat(tactic/assert_exists): user command for assertions about imports (#17416)

kim-em committed 3 years ago

947f7bde

refactor(*): supremum of refactoring PRs #17384 #17398 #17406 #17407 #17408 (#17405)

kim-em committed 3 years ago

ad7038e5

feat(algebra/category/Module): instances for modules over algebras (#13933)

kim-em committed 3 years ago

6cc39472

refactor(topology/sheaf_condition): remove has_products for restriction to open subspace (#17361)

alreadydone committed 3 years ago

f384f5d1

feat(measure_theory/integral): lintegral_tsum' (#17309)

AlexKontorovich committed 3 years ago

946ab799

feat(data/set/basic): add `mem_ite_empty_left/right` (#17264)

RemyDegenne committed 3 years ago

cbdbfd72

feat(topology/metric_space/hausdorff_distance): A `cthickening` is an intersection of `thickenings` (#17258)

YaelDillies committed 3 years ago

89fd6afc

ci(bors): set update_base_for_deletes (#17410)

eric-wieser committed 3 years ago

6dded232

chore(*): add mathlib3 synchronization labels (#17314)

kim-em committed 3 years ago

d82d6e26

feat(linear_algebra/affine_space/midpoint): `midpoint_eq_left_iff`, `midpoint_eq_right_iff` (#17385)

jsm28 committed 3 years ago

29014241

chore(probability/process/stopping): generalize lemmas about nat-indexed processes to generic types (#17379)

RemyDegenne committed 3 years ago

bea6c853

feat(topology/algebra/group): `•` lemmas (#17383)

YaelDillies committed 3 years ago

1f195436

feat(data/list/basic): add `list.chain'_append` and corollaries (#17308)

urkud committed 3 years ago

77b0b36c

chore(data/set/basic): Make `set.nonempty.ne_empty` an alias (#17382)

YaelDillies committed 3 years ago

4a38f249

chore(logic/lemmas): freeze file (#17380)

mcdoll committed 3 years ago

ac2e4c07

chore: freeze function.conjugate (#17351)

joneugster committed 3 years ago

48d37303

feat(linear_algebra/matrix/to_lin): add `linear_map.to_matrix_distrib_mul_action_to_linear_map` (#17337)

eric-wieser committed 3 years ago

97a63eaa

chore: freeze data.bool.basic (#17324)

kbuzzard committed 3 years ago

9eb1e2af

feat(order/antichain): Weak antichains (#17075)

YaelDillies committed 3 years ago

00d9016e

refactor(*): supremum of several recent refactoring PRs (#17381)

kim-em committed 3 years ago

f7707875

feat(group_theory/*): Add `finite` instances (#17377)

tb65536 committed 3 years ago

34fa1f81

chore(data/finset/prod): golf a proof (#17373)

eric-wieser committed 3 years ago

382bdab6

chore(data/nat/cast): remove spurious imports (#17336)

kim-em committed 3 years ago

ed04b515

chore(category_theory): better definitional properties for kernel_lift (#17328)

joelriou committed 3 years ago

4dabfb92

feat(combinatorics/simple_graph/connectivity): Transfer walks from a `simple_graph` to another (#17326)

bottine committed 3 years ago

7a5f20f4

feat(category_theory/limits/shapes/binary_products): API for binary (co)products (#17317)

erdOne committed 3 years ago

fec1d95f

feat(src/topology/category/Top/limits): Coproducts in `Top`. (#17282)

erdOne committed 3 years ago

480c757a

feat(data/{seq,stream}): enum and some helper API (#15790)

pechersky committed 3 years ago

22f02c16

Older