leanprover-community/mathlib3

Pull Requests Commits

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

feat(algebraic_geometry): Localization map is an embedding. (#10471)

erdOne committed 4 years ago

461051ae

feat(algebraic_geometry): Isomorphisms of presheafed space. (#10461)

erdOne committed 4 years ago

6bd6b45e

feat(linear_algebra/orientation): orientations of modules and rays in modules (#10306)

jsm28 committed 4 years ago

f8f28da0

feat(analysis/convex/[basic, topology]): generalize path connectedness of convex sets to topological real vector spaces (#10011)

ADedecker committed 4 years ago

2bb627fc

feat(ring_theory/polynomial/cyclotomic): `is_root_cyclotomic_iff` (#10422)

ericrbg committed 4 years ago

8915dc8e

feat(category_theory/limits): Lemmas about preserving pullbacks (#10438)

erdOne committed 4 years ago

6f745cd2

feat(algebra/tropical/basic): various API (#10487)

pechersky committed 4 years ago

c791747d

feat(data/finsupp/basic): add `finsupp.prod_congr` and `sum_congr` (#10568)

stuart-presnell committed 4 years ago

ac767452

kex-y committed 4 years ago

c7df6528

feat(data/finsupp/basic): add `nat.cast_finsupp_prod` and 3 others (#10579)

stuart-presnell committed 4 years ago

42d3cbc3

chore(category_theory/sites/*): Adjust some `simp` lemmas. (#10574)

adamtopaz committed 4 years ago

4cfe637b

feat(data/nat/prime): Add lemma `count_factors_mul_of_pos` (#10536)

stuart-presnell committed 4 years ago

cbb2d2c0

feat(data/nat/prime): add coprime_of_prime lemmas (#10534)

BoltonBailey committed 4 years ago

38ae0c96

feat(data/finset/*): Diverse lemmas (#10388)

YaelDillies committed 4 years ago

5e022925

feat(combinatorics/set_family/compression/uv): UV-compression of a set family (#10238)

YaelDillies committed 4 years ago

790d6373

feat(probability_theory/stopping): define filtration and stopping time (#10553)

kex-y committed 4 years ago

17c22094

feat(category_theory/sites/adjunction): Adjunctions between categories of sheaves. (#10541)

adamtopaz committed 4 years ago

68060507

feat(ring_theory/localization): The localization of a localization is a localization. (#10456)

erdOne committed 4 years ago

3e72feb3

chore(*): golf some proofs (#10575)

urkud committed 4 years ago

fed2929b

chore(*): clean up/golf proofs with unneeded or case splits (#10569)

alexjbest committed 4 years ago

665c13a4

doc(group_theory/index): add a theorem name and fix a to_additive (#10564)

alexjbest committed 4 years ago

34758d3f

chore(algebra/order/*): drop some `[nontrivial _]` assumptions (#10550)

urkud committed 4 years ago

70435215

Newer Older