leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 4 years ago

2ec62c7e

fix(algebra/ring): fix diamonds in nat- and int- algebras

eric-wieser committed 4 years ago

7d72f4e0

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

refactor(linear_algebra/charpoly): split in two files (#9485)

riccardobrasca committed 4 years ago

110c740c

refactor(linear_algebra/free_module_pid): move linear_algebra/free_module_pid to linear_algebra/free_module/pid (#9482)

riccardobrasca committed 4 years ago

1ceebca6

feat(measure_theory/function/ae_eq_of_integral): two ennreal-valued function are a.e. equal if their integrals agree (#9372)

kex-y committed 4 years ago

fa7fdcae

feat(data/finset/interval): API for `finset.Ixx` (#9495)

YaelDillies committed 4 years ago

241aad7b

chore(src/analysis/special_functions/trigonometric/basic) : prove continuity of sin/cos/sinh/cosh without derivatives (#9502)

RemyDegenne committed 4 years ago

f3746ea6

Older