leanprover-community/mathlib3

Pull Requests Commits

chore(data/set/lattice): move basic lemmas to basic files (#17882)

astrainfinita committed 3 years ago

3d954923

chore(data/real/cau_seq{_completion}): add lemmas about pow and smul (#17796)

eric-wieser committed 3 years ago

dce07aeb

feat(group_theory/subgroup/basic): add 2 lemmas (#17987)

urkud committed 3 years ago

6c48d300

chore(field_theory/separable_degree): golf a proof using `wlog` (#17952)

urkud committed 3 years ago

0743cc5d

feat(geometry/euclidean/basic): second intersection of a line and a sphere (#17843)

jsm28 committed 3 years ago

ea9c24f6

feat(geometry/euclidean/angle/oriented/right_angle): trigonometric lemmas (#17683)

jsm28 committed 3 years ago

e8a45253

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

develop short_exact

joelriou committed 3 years ago

b4b2e4e0

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

comp_homology_π_eq_iff

joelriou committed 3 years ago

005af62d

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

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

YaelDillies committed 3 years ago

b3f25363

Newer Older