leanprover-community/mathlib

Pull Requests Commits

Some experiments in matching

stuart-presnell committed 4 years ago

86faa5f7

Setting up some basic `ε_NFA`s

stuart-presnell committed 4 years ago

c8784701

feat(data/finsupp/basic): add two versions of `finsupp.mul_prod_erase` (#10708)

stuart-presnell committed 4 years ago

e5a844e1

feat(algebra/algebra): instantiate `ring_hom_class` for `alg_hom` (#10853)

Vierkantor committed 4 years ago

c9fe6d1a

feat(ring_theory/noetherian): fg_pi (#10845)

eric-wieser committed 4 years ago

ba24b38b

feat(data/set/function): Cancelling composition on a set (#10803)

YaelDillies committed 4 years ago

5a598003

feat(combinatorics/configuration): New file (#10773)

tb65536 committed 4 years ago

6838233f

feat(data/nat/count): The count function on naturals (#9457)

kim-em committed 4 years ago

8743573e

chore(algebra/associated): split off dependencies of `big_operators` (#10848)

Vierkantor committed 4 years ago

081cb8ab

feat(algebra/big_operators/basic): add finset.prod_to_list (#10842)

Jlh18 committed 4 years ago

862a68c9

feat(topology/subset_properties): open/closed sets are locally compact spaces (#10844)

urkud committed 4 years ago

5558fd9f

feat(combinatorics/simple_graph/basic): Incidence set lemmas (#10839)

YaelDillies committed 4 years ago

b100af69

refactor(category_theory/sites/*): Redefine the category of sheaves. (#10678)

adamtopaz committed 4 years ago

9f9015c6

fix(ring_theory/ideal/basic): remove universe restriction (#10843)

eric-wieser committed 4 years ago

601f2ab7

chore(field_theory/ratfunc): to_fraction_ring_ring_equiv (#10806)

eric-wieser committed 4 years ago

905d887f

chore(field_theory/ratfunc): has_scalar in terms of localization (#10828)

pechersky committed 4 years ago

eeef771d

feat(data/set/function): Congruence lemmas for `monotone_on` and friends (#10817)

YaelDillies committed 4 years ago

542471fd

feat(ring_theory/local_property): Being reduced is a local property. (#10734)

erdOne committed 4 years ago

b5b19a69

chore(analysis/mean_inequalities_pow): nnreal versions of some ennreal inequalities (#10836)

hrmacbeth committed 4 years ago

68ced9a9

feat(measure_theory/measure): new class is_finite_measure_on_compacts (#10827)

sgouezel committed 4 years ago

d212f3eb

feat(category_theory/adjunction/evaluation): Evaluation has a left and a right adjoint. (#10793)

adamtopaz committed 4 years ago

87e2f24b

chore(data/polynomial/field_division): beta-reduce (#10835)

gebner committed 4 years ago

8e4b3b0f

chore(*): tweaks taken from gh-8889 (#10829)

eric-wieser committed 4 years ago

5a835b7b

feat(analysis/normed_space/basic): formula for `c • sphere x r` (#10814)

urkud committed 4 years ago

8218a788

feat(topology/metric_space/isometry): (pre)image of a (closed) ball or a sphere (#10813)

urkud committed 4 years ago

b82c0d25

feat(topology/metric_space/hausdorff_distance): add more topological properties API to thickenings (#10661)

kkytola committed 4 years ago

21c9d3b3

chore(topology/continuous_function/bounded): remove extra typeclass assumption (#10823)

hrmacbeth committed 4 years ago

ef69cac1

feat(algebra/module/linear_map): interaction of linear maps and pointwise operations on sets (#10821)

sgouezel committed 4 years ago

00c55f5e

feat(analysis/special_functions/complex): range of `complex.exp (↑x * I)` (#10816)

urkud committed 4 years ago

dfb78f7e

feat(analysis/mean_inequalities): corollary of Hölder inequality (#10789)

hrmacbeth committed 4 years ago

81e58c9e

Older