leanprover-community/mathlib

Pull Requests Commits

eric-wieser/deriv-exp-prework/with-elemental_algebra

eric-wieser committed 2 years ago

2b01f7e0

eric-wieser committed 2 years ago

aadef76b

LaTeX docstring

eric-wieser committed 2 years ago

3754ef36

eric-wieser committed 2 years ago

612de6ab

eric-wieser committed 2 years ago

fea00f3d

eric-wieser committed 2 years ago

bf4d1fb8

feat(analysis/special_functions/exponential): derivative of `u ↦ exp 𝕂 (u • x)`

eric-wieser committed 2 years ago

8733d438

feat(analysis/calculus/mean_value): functions are equal if their derivatives and a point are equal (#19059)

eric-wieser committed 2 years ago

75e7fca5

chore(analysis/special_functions/non_integrable): split (#19047)

hrmacbeth committed 2 years ago

55ec6e9a

feat(field_theory/splitting_field): fix the diamond (#18857)

ericrbg committed 2 years ago

b353176c

feat(probability/kernel/disintegration): disintegration of finite measures on product spaces (#18834)

RemyDegenne committed 2 years ago

3b88f400

chore(linear_algebra/basis): `simp` lemmas about `basis.equiv_fun` (#19021)

eric-wieser committed 2 years ago

13bce9a6

chore(*): add mathlib4 synchronization comments (#19057)

github-actions[bot] committed 2 years ago

4280f5f3

feat(combinatorics/simple_graph): Szemerédi's Regularity Lemma (#11000)

YaelDillies committed 2 years ago

1d4d3ca5

chore(data/multiset/pi): correct names and reorder (#19050)

eric-wieser committed 2 years ago

b2c89893

chore(*): add mathlib4 synchronization comments (#19055)

github-actions[bot] committed 2 years ago

1b0a28e1

chore(*): add mathlib4 synchronization comments (#19042)

github-actions[bot] committed 2 years ago

33c67ae6

refactor(topology): fix definition of residual (#18962)

Felix-Weilacher committed 2 years ago

b9e46fe1

feat(measure_theory/function/l1_space): generalize from fields to rings (#19052)

eric-wieser committed 2 years ago

9b33e5f3

feat(combinatorics/simple_graph/regularity): Increment partition (#19051)

YaelDillies committed 2 years ago

bf7ef0e8

feat(combinatorics/simple_graph/regularity/chunk): Partition of a part (#18371)

YaelDillies committed 2 years ago

f51de876

chore(.github/workflows): don't rely on linkifier in maintainer merge messages (#19046)

kim-em committed 2 years ago

ef7403fe

chore(ring_theory/localization/away): split (#19041)

kim-em committed 2 years ago

a7c017d7

chore(analysis/convex/cone/basic): split (#19043)

hrmacbeth committed 2 years ago

915591b2

feat(linear_algebra/matrix/charpoly/minpoly): `minpoly` is unaffected by `to_lin` and `to_matrix` (#19036)

eric-wieser committed 2 years ago

7ae139f9

chore(measure_theory/{constructions/prod,measure/lebesgue}): split (#19039)

hrmacbeth committed 2 years ago

fd5edc43

feat(topology/algebra/module/star): continuity results for star_modules (#19037)

eric-wieser committed 2 years ago

aa666983

chore(measure_theory/special_functions/basic): split (#19040)

hrmacbeth committed 2 years ago

83a66c87

chore(category_theory/monoidal/types): split file (#19035)

kim-em committed 2 years ago

95a87616

chore(algebra/category/Module/monoidal): split file (#19034)

kim-em committed 2 years ago

74403a3b

Older