leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'master' into YK-cardinal-to-enat

urkud committed 3 years ago

6386b9b8

feat(analysis/convex/between): betweenness and affine combinations (#17912)

jsm28 committed 3 years ago

ba2245ed

refactor(measure_theory/measurable_space): utilize measurable_embedding more (#17980)

Felix-Weilacher committed 3 years ago

09fa0b0c

fix(scripts/port_comments): handle moved files (#17978)

eric-wieser committed 3 years ago

a7aa4a2e

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

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

refactor(measure_theory/group/fundamental_domain): Use `pairwise` (#17928)

YaelDillies committed 3 years ago

d5ca915d

urkud committed 3 years ago

f539d250

Merge branch 'master' into YK-cardinal-to-enat

urkud committed 3 years ago

a580f59c

chore(order/monovary): Move (#17946)

YaelDillies committed 3 years ago

b3f25363

feat(measure_theory/covering) weaken sigma_compact_space to second_countable_topology (#17960)

sgouezel committed 3 years ago

d012cd09

chore(data/finset/lattice): Protect ambiguous lemmas (#17938)

YaelDillies committed 3 years ago

302eab4f

feat(combinatorics/simple_graph/*): some more `from_edge_set` and `edge_set` lemmas (#17723)

bottine committed 3 years ago

e3a8dff0

fix(algebra/opposites): fix types in unop_div (#17955)

kbuzzard committed 3 years ago

ac3910d7

chore(data/set/image): Turn lemma around (#17945)

YaelDillies committed 3 years ago

616e053d

Older