leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/limits/shapes): Multiequalizer is the equalizer (#10267)

erdOne committed 4 years ago

a5866810

feat(topology/metric_space): range of a cauchy seq is bounded (#10423)

urkud committed 4 years ago

6dddef28

feat(algebra/algebra/spectrum): define spectrum and prove basic prope... (#10390)

j-loreaux committed 4 years ago

f684f612

feat(measure_theory/integral/interval_integral): add an alternative definition (#10380)

urkud committed 4 years ago

e59e03f1

feat(data/nat/prime): prime divisors (#10318)

stuart-presnell committed 4 years ago

2f5af98b

feat(analysis/calculus/parametric_integral): generalize, rename (#10397)

urkud committed 4 years ago

317483a6

fix(undergrad.yaml): reinstate deleted entry (#10416)

hrmacbeth committed 4 years ago

d2ebcad1

feat(data/finset/basic) eq_of_mem_singleton (#10414)

isadofschi committed 4 years ago

c8961621

chore(algebra/opposites): split group actions and division_ring into their own files (#10383)

eric-wieser committed 4 years ago

d8d0c595

feat(data): define a `fun_like` class of bundled homs (function + proofs) (#10286)

Vierkantor committed 4 years ago

2aea9961

feat(ring_theory/roots_of_unity): primitive root lemmas (#10356)

ericrbg committed 4 years ago

7a5fac38

docs(undergrad): add urls in linear algebra (#10415)

PatrickMassot committed 4 years ago

9f075796

chore(data/finset/basic): finset.prod -> finset.product in module docstring (#10413)

kmill committed 4 years ago

9277d4b4

chore(*): golf proofs about `filter.Coprod` (#10400)

urkud committed 4 years ago

d17db717

feat(linear_algebra/bilinear_map): semilinearize bilinear maps (#10373)

dupuisf committed 4 years ago

d98b8e0e

feat(measure_theory/covering/differentiation): differentiation of measures (#10101)

sgouezel committed 4 years ago

8f07d75b

feat(measure_theory): define volume on `complex` (#10403)

urkud committed 4 years ago

8ee634b0

feat(analysis/inner_product_space/projection): orthogonal group is generated by reflections (#10381)

hrmacbeth committed 4 years ago

2168297e

feat(topology/separation): removing a finite set from a dense set preserves density (#10405)

sgouezel committed 4 years ago

e0c0d84a

remove duplicate arguments

dupuisf committed 4 years ago

63c55e9f

add comp instance

dupuisf committed 4 years ago

d544906a

feat(measure_theory): measure preserving maps and integrals (#10326)

urkud committed 4 years ago

55b81f8b

apply won't find instance

dupuisf committed 4 years ago

0052d5f4

dupuisf committed 4 years ago

b2cd4943

feat(data/finset/basic): add filter_erase (#10384)

BoltonBailey committed 4 years ago

2a286527

operator_norm: first pass completed

dupuisf committed 4 years ago

5cb8d13d

feat(data/nat/interval): add Ico_succ_left_eq_erase (#10386)

BoltonBailey committed 4 years ago

32c05079

dupuisf committed 4 years ago

7cd489c9

feat(topology/algebra/infinite_sum): add `has_sum.smul_const` etc (#10393)

urkud committed 4 years ago

b3538bfa

feat(analysis/special_functions/complex/arg): review, golf, lemmas (#10365)

urkud committed 4 years ago

618447fa

Newer Older