leanprover-community/mathlib

Pull Requests Commits

kim-em committed 3 years ago

a1d75616

refactor(algebra/order/ring/basic): split file

kim-em committed 3 years ago

73805281

Merge branch 'algebra_ring_basic2' into algebra_order_ring_basic

kim-em committed 3 years ago

819f8823

kim-em committed 3 years ago

92b230a4

different split

kim-em committed 3 years ago

75ad56a0

kim-em committed 3 years ago

d52c0454

Merge branch 'algebra_hom_equiv' into algebra_order_group_basic

kim-em committed 3 years ago

eb01363b

kim-em committed 3 years ago

944638c9

kim-em committed 3 years ago

38ef930c

refactor(algebra/order/group/basic): split

kim-em committed 3 years ago

a5ce41d8

kim-em committed 3 years ago

20dbc540

refactor(algebra/hom/equiv): split files

kim-em committed 3 years ago

b5f48259

refactor(algebra/order/sub/basic): split defs

kim-em committed 3 years ago

a7ea5c30

Merge branch 'algebra_ring_basic' into algebra_order_group_basic

kim-em committed 3 years ago

41fa17df

refactor(algebra/order/monoid/basic): splits defs and basic

kim-em committed 3 years ago

b02bf9a6

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

refactor(algebra/ring/basic): split out algebra.ring.defs

kim-em committed 3 years ago

e2e45be1

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

Older