leanprover-community/mathlib3

Pull Requests Commits

chore(measure_theory/integral): add `integrable_const` for `interval_integral` (#10410)

urkud committed 4 years ago

28177886

chore(measure_theory/integral): more versions of `integral_finset_sum` (#10394)

urkud committed 4 years ago

3b137447

feat(topology/connected): sufficient conditions for the preimage of a connected set to be connected (#10289)

YaelDillies committed 4 years ago

2ec6de7d

feat(group_theory/exponent): Define the exponent of a group (#10249)

Julian-Kuelshammer committed 4 years ago

e8386bd4

refactor(*): split `order_{top,bot}` from `lattice` hierarchy (#9891)

pechersky committed 4 years ago

cf917732

chore(control/random): Move from `system.random.basic` (#10408)

YaelDillies committed 4 years ago

3fee4b9b

feat(analysis/normed_space/multilinear): add `norm_mk_pi_field` (#10396)

urkud committed 4 years ago

b1a9c2e4

chore(field_theory/separable): generalize theorems (#10337)

ericrbg committed 4 years ago

87b0084b

feat(order/filter/pi): define `filter.pi` and prove some properties (#10323)

urkud committed 4 years ago

9cf6766f

feat(linear_algebra/affine_space/barycentric_coords): barycentric coordinates are ratio of determinants (#10320)

ocfnash committed 4 years ago

33ea4012

feat(algebra/big_operators/finprod): add finprod_div_distrib and finsum_sub_distrib (#10044)

alexjbest committed 4 years ago

d94772bb

chore(measure_theory/integral): generalize `integral_smul_const` (#10411)

urkud committed 4 years ago

ac712929

chore(data/complex): add a few simp lemmas (#10395)

urkud committed 4 years ago

8f681f12

feat(data/complex/exponential): Add lemma add_one_le_exp (#10358)

isadofschi committed 4 years ago

4d5d7708

feat(algebraic_geometry, category_theory): SheafedSpace has colimits (#10401)

erdOne committed 4 years ago

6050f9df

refactor(ring_theory/sub[semi]ring): move pointwise instances to their own file (#10347)

eric-wieser committed 4 years ago

ca7347c4

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

Newer Older