leanprover-community/mathlib3

Pull Requests Commits

doc(data/list/*): Elaborate module docstrings (#9076)

BoltonBailey committed 4 years ago

96c1d69b

chore(ring_theory/noetherian): fix URL (#9149)

ChrisHughes24 committed 4 years ago

f75bee3f

feat(data/real/ennreal): add `contravariant_class ennreal ennreal (+) (<)` (#9143)

urkud committed 4 years ago

55aaebe1

chore(analysis/calculus/*): add `filter.eventually_eq.deriv` etc. (#9131)

urkud committed 4 years ago

c0693ca0

feat(data/real/ennreal): add ennreal.to_(nn)real_inv and ennreal.to_(nn)real_div (#9144)

RemyDegenne committed 4 years ago

1605b859

split(analysis/convex/combination): split off `analysis.convex.basic` (#9115)

YaelDillies committed 4 years ago

b9ad7333

feat(interval_integral): generalize change of variables (#8869)

fpvandoorn committed 4 years ago

62de5912

feat(measure_theory/function/conditional_expectation): conditional expectation of an indicator (#8920)

RemyDegenne committed 4 years ago

6823886c

feat(data/finsupp): more lemmas about `α →₀ ℕ` (#9137)

urkud committed 4 years ago

241ee9ee

chore(data/mv_polynomials): golf, add a lemma (#9132)

urkud committed 4 years ago

e0093544

feat(data/mv_polynomial/equiv): empty_equiv (#9122)

ChrisHughes24 committed 4 years ago

d72119cb

chore(ring_theory/artinian): typo (#9140)

ChrisHughes24 committed 4 years ago

f318e5d6

chore(combinatorics/simple_graph): rename sym to symm (#9134)

kmill committed 4 years ago

579ca5ed

refactor(topology/path_connected): make `path` extend `C(I, X)` (#9133)

shingtaklam1324 committed 4 years ago

919aad21

chore(algebra/ordered_smul): reduce instance assumptions & delete duplicated instances (#9130)

YaelDillies committed 4 years ago

84136229

feat(algebra/ordered_monoid): order_embedding.mul_left (#9127)

kim-em committed 4 years ago

2e9f708d

feat(measure_theory/measure/set_integral): new lemma integral_Union (#9093)

sgouezel committed 4 years ago

4c96b8a5

chore(algebra/group/basic): add 3 `simp` attrs (#9050)

urkud committed 4 years ago

426227d4

feat(ring_theory/algebraic): is_algebraic_of_larger_base (#9109)

ChrisHughes24 committed 4 years ago

e4ca1175

refactor(analysis/convex/basic): generalize segments to vector spaces (#9094)

YaelDillies committed 4 years ago

7500529f

feat(combinatorics/simple_graph/adj_matrix): more lemmas (#9021)

l534zhan committed 4 years ago

0e014ba5

feat(data/mv_polynomial): mv_polynomial.subsingleton (#9124)

ChrisHughes24 committed 4 years ago

a949b57b

refactor(algebra/group/units): better defeq for is_unit.unit (#9112)

sgouezel committed 4 years ago

92e7bbe9

feat(topology/compact_open): express the compact-open topology as an Inf of topologies (#9106)

hrmacbeth committed 4 years ago

574864d3

feat(ring_theory/dedekind_domain): add proof that `I \sup J` is the product of `factors I \inf factors J` for `I, J` ideals in a Dedekind Domain (#9055)

Paul-Lez committed 4 years ago

d2afdc59

feat(ring_theory/artinian): Artinian modules (#9009)

ChrisHughes24 committed 4 years ago

6d2cbf9d

feat(topology/homotopy): Define homotopy between functions (#8947)

shingtaklam1324 committed 4 years ago

2410c1ff

feat(measure_theory/integral/bochner): generalize the Bochner integral construction (#8939)

RemyDegenne committed 4 years ago

5ce9280f

feat(linear_algebra/matrix/transvection): matrices are generated by transvections and diagonal matrices (#8898)

sgouezel committed 4 years ago

56ff42bd

feat(ring_theory/norm): `norm R x = 0 ↔ x = 0` (#9042)

Vierkantor committed 4 years ago

a057a8e9

Newer Older