leanprover-community/mathlib

Pull Requests Commits

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

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

chore(*): more cleanups of by_cases (#10549)

alexjbest committed 4 years ago

0f12400c

feat(*): assorted `finset` lemmas (#10566)

ericrbg committed 4 years ago

c09501db

feat(data/nat/prime): Add lemma `factors_count_pow` (#10554)

stuart-presnell committed 4 years ago

cc604706

feat(analysis/normed_space/star and data/complex/is_R_or_C): register instances of `cstar_ring` (#10555)

j-loreaux committed 4 years ago

599a5118

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

leanprover-community-bot committed 4 years ago

3f7d0cfd

chore(analysis/mean_inequalities[_pow]): use vector notation (#10546)

hrmacbeth committed 4 years ago

49f8b6b8

feat(algebra/char_p/two): couple more lemmas + 🏌️ (#10467)

eric-wieser committed 4 years ago

b876e76b

doc(data/stream/defs): add docstrings to most defs (#10547)

urkud committed 4 years ago

cd69351b

refactor(algebra/group/basic): Migrate `add_group` section into `group` section (#10532)

mans0954 committed 4 years ago

8bce7eb0

Newer Older