Commits leanprover-community/mathlib3

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

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