leanprover-community/mathlib3

Pull Requests Commits

ADedecker committed 2 years ago

090c3f0a

ADedecker committed 2 years ago

e56649fb

Merge branch 'AD_uniform_convergence_generated_bornology' into AD_uniform_convergence_complete

ADedecker committed 2 years ago

fad5afdd

ADedecker committed 2 years ago

652e38a0

Main lemma done

ADedecker committed 2 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

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

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

Felix-Weilacher committed 3 years ago

138f1db8

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

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

Multramate committed 3 years ago

c5c7e276

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

ADedecker committed 3 years ago

dcf22508

feat(ring_theory/ideal/local_ring): add lemmas about local_ring.residue_field.map (#17969)

mkaratarakis committed 3 years ago

758a6a4e

chore(number_theory/divisors): golf (#17954)

urkud committed 3 years ago

c2337ec8

feat(combinatorics/quiver/*): More edge reversal constructions (#17665)

bottine committed 3 years ago

706d88f2

feat(measure_theory/integral/layercake): Add versions of layercake formula with strict inequality. (#17920)

kkytola committed 3 years ago

11bb0c91

feat(measure_theory/measure/measure_space): A `measurable_equiv` is `quasi_measure_preserving` (#17774)

YaelDillies committed 3 years ago

2c5df64a

feat(dynamics/ergodic/ergodic): expand ergodic map API for finite measures (#17864)

ocfnash committed 3 years ago

809e920e

Older