leanprover-community/mathlib

Pull Requests Commits

erdOne committed 4 years ago

e5fc7099

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

erdOne committed 4 years ago

79f44e82

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

feat(data/sigma{lex,order}): Lexicographic and disjoint orders on a sigma type (#10552)

YaelDillies committed 4 years ago

56c9cab5

feat(category_theory/limits): Walking parallel pair equiv to its op. (#10516)

erdOne committed 4 years ago

d62b5178

feat(algebra/gcd_monoid/*): assorted lemmas (#10508)

ericrbg committed 4 years ago

c151a121

feat(data/nat/basic): Monotonicity of `nat.find_greatest` (#10507)

YaelDillies committed 4 years ago

c093d04d

feat(topology/urysohns_bounded): +2 versions of Urysohn's lemma (#10479)

urkud committed 4 years ago

00e9e90a

feat(category_theory/adjunction): Added simp lemmas for `left_adjoint_uniq` and `right_adjoint_uniq` (#10551)

erdOne committed 4 years ago

403d9c0e

feat(topology/algebra/group): group topologies on a given group form a complete lattice (#10531)

mariainesdff committed 4 years ago

30185dca

feat(algebra/module): push forward the action of `R` on `M` along `f : R → S` (#10502)

Vierkantor committed 4 years ago

cfecf720

Older