leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'AD_uniform_convergence_complete' into AD_Ascoli

ADedecker committed 2 years ago

5682804a

ADedecker committed 3 years ago

e56649fb

Merge branch 'AD_uniform_convergence_generated_bornology' into AD_uniform_convergence_complete

ADedecker committed 3 years ago

fad5afdd

ADedecker committed 3 years ago

652e38a0

Main lemma done

ADedecker committed 3 years ago

5b2313e3

ADedecker committed 3 years ago

e80bbbe4

ADedecker committed 3 years ago

ad6bbd2f

ADedecker committed 3 years ago

e791b928

ADedecker committed 3 years ago

0c945817

ADedecker committed 3 years ago

1fce757a

First part done

ADedecker committed 3 years ago

ff0d0dd2

ADedecker committed 3 years ago

4cdb798b

Some progress and experiments

ADedecker committed 3 years ago

8c1e932f

chore(algebraic_geometry/elliptic_curve/weierstrass): add disclaimer for coordinate_ring irreducibility (#17977)

Multramate committed 3 years ago

550b5853

feat(measure_theory/measure/portmanteau): Add lemmas in preparation of implication from Borel condition. (#17962)

kkytola committed 3 years ago

d9767b54

feat(algebraic_geometry/EllipticCurve/weierstrass): define Weierstrass polynomials and prove basic facts (#17631)

Multramate committed 3 years ago

b7487a0e

chore(data/polynomial/derivative): replace n by C n (#17911)

Multramate committed 3 years ago

bbeb185d

feat(analysis/locally_convex): locally convex hausdorff spaces (#17937)

LukasMias committed 3 years ago

d2617e08

ADedecker committed 3 years ago

713045bd

feat(algebra/big_operators/basic): Sum of `ite` (#16825)

YaelDillies committed 3 years ago

d4f69d96

ADedecker committed 3 years ago

5c1efc81

feat(topology): add basics of perfect sets (#17492)

Felix-Weilacher committed 3 years ago

138f1db8

Only consider things in the union

ADedecker committed 3 years ago

97960182

feat(topology/instances): add_circle = interval with ends identified (#17889)

loefflerd committed 3 years ago

04206afe

feat(measure_theory/group/fundamental_domain): Interior of a fundamental domain (#17533)

YaelDillies committed 3 years ago

bfc28c4b

ADedecker committed 3 years ago

1585fd28

Working version!

ADedecker committed 3 years ago

2d136b55

feat(data/polynomial/basic): add C_ne_zero (#17970)

Multramate committed 3 years ago

c5c7e276

ADedecker committed 3 years ago

baa51dda

Split `infinite_of_mem_nhds` to extract a useful lemma (#17971)

ADedecker committed 3 years ago

dcf22508

Older