Commits leanprover-community/mathlib

feat(data/fin/interval): Finite intervals in `fin n` (#9523)

YaelDillies committed 4 years ago

a07d1de4

feat(probability_theory/notation): add notations for expected value, conditional expectation (#9469)

RemyDegenne committed 4 years ago

15d987a3

feat(measure_theory/covering/besicovitch_vector_space): vector spaces satisfy the assumption of Besicovitch covering theorem (#9461)

sgouezel committed 4 years ago

ab7d2519

feat(analysis/special_functions): real derivs of `complex.exp` and `complex.log` (#9422)

urkud committed 4 years ago

b6f94a93

feat(ring_theory/algebraic_independent): Existence of transcendence bases and rings are algebraic over transcendence basis (#9377)

ChrisHughes24 committed 4 years ago

1faf964e

feat(order/jordan_holder): Jordan Hölder theorem (#8976)

ChrisHughes24 committed 4 years ago

8a05dca7

feat(linear_algebra/matrix/general_linear_group): GL(n, R) (#8466)

CBirkbeck committed 4 years ago

abe81bcb

feat(topology/algebra): nonarchimedean filter bases (#9511)

PatrickMassot committed 4 years ago

edb22fef

feat(data/nat/interval): finite intervals of naturals (#9507)

YaelDillies committed 4 years ago

6bd6afaf

feat(linear_algebra/free_module/strong_rank_condition): add `comm_ring_strong_rank_condition` (#9486)

riccardobrasca committed 4 years ago

dc1b045a

feat(category_theory/sites/*): Cover-lifting functors on sites (#9431)

erdOne committed 4 years ago

6a6b4d05

feat(field_theory/algebraic_closure): versions of exists_aeval_eq_zero for rings (#9517)

ChrisHughes24 committed 4 years ago

d677c298

chore(data/set/lattice): fix name (#9520)

sgouezel committed 4 years ago

52495a0f

split(order/monotone): split off `order.basic` (#9518)

YaelDillies committed 4 years ago

465508fc

feat(algebra/order): exists_square_le (#9513)

PatrickMassot committed 4 years ago

c0f7c56e

feat(topology/algebra): Cauchy filters on groups (#9512)

PatrickMassot committed 4 years ago

bc5a081f

chore(*): use dot-notation for is_conj.symm and is_conj.trans (#9498)

jcommelin committed 4 years ago

44f4d708

feat(order/basic): define `is_top` and `is_bot` (#9493)

urkud committed 4 years ago

c1936c1f

feat(group_theory/subgroup): mk lemmas (#9514)

PatrickMassot committed 4 years ago

e789ad31

feat(analysis/convex/combination): lemmas connecting convex hull with affine combinations and barycentric coordinates (#9499)

ocfnash committed 4 years ago

d2608945

refactor(ring_theory/unique_factorization_domain): rename unique_factorization_monoid.factors (#9503)

Ruben-VandeVelde committed 4 years ago

cff99277

feat(group_theory/quotient_group): if a quotient is trivial then the subgroup is the whole group (#9092)

CBirkbeck committed 4 years ago

18e7f914

feat(topology/basic): interior of finite intersection is intersection of interiors (#9508)

ocfnash committed 4 years ago

55c30c69

feat(analysis/normed_space/add_torsor_bases): barycentric coordinates are continuous (#9515)

ocfnash committed 4 years ago

2807d83e

feat(analysis/special_functions/exp_log): prove continuity of exp without derivatives (#9501)

RemyDegenne committed 4 years ago

7d83ff15

feat(analysis/convex/function): helper lemmas and general cleanup (#9438)

YaelDillies committed 4 years ago

5f803fae

chore(topology/*): more lemmas about `dense`/`dense_range` (#9492)

urkud committed 4 years ago

7b022774

chore(measure_theory): move, deduplicate (#9489)

urkud committed 4 years ago

c46a04a3

chore(ring_theory/ideal): some simp attributes (#9487)

PatrickMassot committed 4 years ago

a97e86a6

docs(measure_theory/integral/lebesgue): Add "Markov's inequality" to the doc string of `mul_meas_ge_le_lintegral` (#9506)

kex-y committed 4 years ago

e60dc2bb