leanprover-community/mathlib

Pull Requests Commits

AlexKontorovich committed 4 years ago

ea263be5

rearrange for finite measure rather than compact

hrmacbeth committed 4 years ago

c633d388

finish conversion

hrmacbeth committed 4 years ago

dc533a8f

AlexKontorovich committed 4 years ago

c085718c

urkud committed 4 years ago

82ccbe68

Merge branch 'master' into YK-integral-periodic

urkud committed 4 years ago

e986098d

feat(analysis/asymptotics): Generalize superpolynomial decay using limits instead of big O (#10296)

dtumad committed 4 years ago

daf30fd7

urkud committed 4 years ago

accf4d6a

Merge branch 'YK-integral-fundamental' into YK-integral-periodic

urkud committed 4 years ago

ae413268

Merge branch 'master' into YK-integral-fundamental

urkud committed 4 years ago

3b890c7b

fix(tactic/cancel_denoms): remove debug code (#10434)

robertylewis committed 4 years ago

18e55105

feat(measure_theory/group/fundamental_domain): prove equality of integrals (#10448)

urkud committed 4 years ago

b29b9528

feat(measure_theory/integral): dominated convergence for a series (#10398)

urkud committed 4 years ago

563f8c4f

refactor(algebra.abs): Introduce `has_pos_part` and `has_neg_part` classes (#10420)

mans0954 committed 4 years ago

132833b7

feat(linear_algebra/multilinear/basic): multilinear maps with respect to an empty family are all constant (#10433)

ocfnash committed 4 years ago

09b4bfc9

refactor(topology,algebraic_geometry): use bundled maps here and there (#10447)

urkud committed 4 years ago

d487d650

feat(topology/uniform_space/uniform_convergence): slightly generalize theorems (#10444)

urkud committed 4 years ago

3590dc29

feat(topology/sheaves): Generalized some lemmas. (#10440)

erdOne committed 4 years ago

8d07dbf4

chore(ring_theory/polynomial/cyclotomic): use `ratfunc` (#10421)

Vierkantor committed 4 years ago

a086daa5

feat(category_theory/limits): Results about (co)limits in Top (#9985)

erdOne committed 4 years ago

6cb52e67

Merge branch 'YK-smul-inv-meas' into YK-integral-fundamental

urkud committed 4 years ago

8b7cad0c

Merge branch 'master' into YK-smul-inv-meas

urkud committed 4 years ago

4782694e

chore(topology): add 2 missing `inhabited` instances (#10446)

urkud committed 4 years ago

d267b6ca

urkud committed 4 years ago

d764d64e

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

leanprover-community-bot committed 4 years ago

1c001794

Merge branch 'YK-smul-inv-meas' into YK-integral-fundamental

urkud committed 4 years ago

a1d5a2c2

feat(measure_theory): TC for smul-invariant measures (#10325)

urkud committed 4 years ago

f578d1d6

Add `docs`, rename, add `tfae`

urkud committed 4 years ago

638acb28

feat(ring_theory/adjoin/basic): add adjoin_induction' and adjoin_adjoin_coe_preimage (#10427)

riccardobrasca committed 4 years ago

0cbba1a4

feat(analysis): derivative of a parametric interval integral (#10404)

urkud committed 4 years ago

c192937f

Older