Commits leanprover-community/mathlib3

feat(analysis/locally_convex/bounded): characterize boundedness using sequences (#17688)

ADedecker committed 3 years ago

ac1e2e08

chore(data/nat/modeq): split out lemmas about lists (#18004)

hrmacbeth committed 3 years ago

3813d4ea

chore(*): fix docs and a name generated by to_additive (#18002)

alreadydone committed 3 years ago

cfa57f46

feat(number_theory/number_field/embeddings) : add infinite_places (#17844)

xroblot committed 3 years ago

51c6beb4

refactor(ring_theory/ideal/quotient): extract a `ring_con` structure (#17833)

eric-wieser committed 3 years ago

b26e15a4

feat(*): bump to lean 3.50.1 (#17995)

gebner committed 3 years ago

2f3994e1

chore(analysis/bounded_variation): replace uses of `linarith` (#17998)

bottine committed 3 years ago

a149cb73

feat(group_theory/order_of_element): a condition on o(x) and o(y) that implies o(xy)=o(y) (#17997)

alreadydone committed 3 years ago

412b1515

feat(linear_algebra/affine_space/affine_subspace): induction principle (#17520)

datokrat committed 3 years ago

d55a93d8

feat(measure_theory/measurable_space) add measurable Schroeder-Bernstein (#17988)

Felix-Weilacher committed 3 years ago

207cfac9

feat(analysis/normed_space/compact_operator): generalize `is_closed_set_of_compact_operator` (#17715)

ADedecker committed 3 years ago

026bed67

refactor(algebra/group_with_zero/defs): use `is_*cancel_mul_zero` (#17963)

urkud committed 3 years ago

a47cda96

chore(data/set/pointwise): split file and reduce imports (#17991)

jcommelin committed 3 years ago

9116dd67

feat(measure_theory/kernel/basic): define kernels and classes of kernels (Markov, finite, s-finite) (#17976)

RemyDegenne committed 3 years ago

56f4cd1e

feat(*): add various results split out from proof of Gallagher's theorem (#17985)

ocfnash committed 3 years ago

5cc2dfdd

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

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