leanprover-community/mathlib

Pull Requests Commits

kex-y committed 4 years ago

4cda52e7

Merge branch 'master' of https://github.com/leanprover-community/mathlib into JasonKYi/stopped_process

kex-y committed 4 years ago

b9034baf

feat(analysis.normed_space.lattice_ordered_group): Add `two_inf_sub_two_inf_le`, `two_sup_sub_two_sup_le` and supporting lemmas (#10514)

mans0954 committed 4 years ago

1376f53d

chore(data/nat/prime): golf some proofs (#10599)

Ruben-VandeVelde committed 4 years ago

cd2230b4

fix(tactic/abel): handle smul on groups (#10587)

digama0 committed 4 years ago

bddc16a5

feat(probability_theory/stopping): generalize a lemma (#10598)

kex-y committed 4 years ago

46e9a235

feat(data/finset/lattice): add sup_eq_bot_iff and inf_eq_top_iff (#10596)

alexjbest committed 4 years ago

1e897458

feat(data/(mv_)polynomial): add aeval_prod and aeval_sum for (mv_)polynomial (#10594)

alexjbest committed 4 years ago

92fafba2

feat(category_theory/limits): Strict terminal objects. (#10582)

erdOne committed 4 years ago

4de07731

feat(topology/sheaves): The empty component of a sheaf is terminal (#10578)

erdOne committed 4 years ago

d45708fc

chore(algebra/lattice_ordered_group): review (names, spaces, golf...) (#10595)

RemyDegenne committed 4 years ago

1e18e93d

fix(tactic/ring): bugfixes in ring_nf (#10572)

digama0 committed 4 years ago

a7b4018a

feat(algebraic_geometry): Explicit description of the colimit of presheafed spaces. (#10466)

erdOne committed 4 years ago

df931664

feat(algebraic_geometry): Open immersions of presheafed spaces (#10437)

erdOne committed 4 years ago

b7ed03f9

feat(algebra/monoid_algebra/grading): internal graded structure for an arbitrary degree function (#10435)

yuma-mizuno committed 4 years ago

2f44ac8f

feat(category_theory/*): Representably flat functors (#9519)

erdOne committed 4 years ago

f0a1cd1a

chore(*): protect `to_fun` and `map_{add,zero,mul,one,div}` (#10580)

Vierkantor committed 4 years ago

8bb26a72

feat(topology/metric_space/hausdorff_distance): add definition and lemmas about closed thickenings of subsets (#10542)

kkytola committed 4 years ago

235e5839

feat(data/mv_polynomial): add total_degree_add_of_total_degree_lt (#10571)

alexjbest committed 4 years ago

65335003

feat(src/algebra/gcd_monoid,src/ring_theory): add some exists_associated_pow_of_mul_eq_pow variants (#10560)

Ruben-VandeVelde committed 4 years ago

672e2b20

feat(data/fintype/order): complete order instances for fintype (#7123)

b-mehta committed 4 years ago

89697a24

feat(order/bounded_order): a few more `simp` lemmas (#10533)

urkud committed 4 years ago

e0c27fe4

feat(analysis/convex/star): Star-convex sets (#10524)

YaelDillies committed 4 years ago

970f0746

doc(algebra.lattice_ordered_group): Remove verbose docstrings (#10468)

mans0954 committed 4 years ago

44b649ca

chore(int/*): dedup lemma (#10583)

ericrbg committed 4 years ago

2648e685

feat(category_theory/limits): The product is the pullback over the terminal objects. (#10581)

erdOne committed 4 years ago

0453320a

chore(topology/{metric_space,instances/real}): cleanup (#10577)

urkud committed 4 years ago

bfccd1b8

feat(ring_theory): Nilradical and reduced ring (#10576)

erdOne committed 4 years ago

158263c1

refactor(data/stream): swap args of `stream.nth` (#10559)

urkud committed 4 years ago

c176aa5d

chore(group_theory/*): additivise! (#10557)

ericrbg committed 4 years ago

55b64b61

Older