leanprover-community/mathlib3

Pull Requests Commits

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

github-actions[bot] committed 3 years ago

fe8d0ff4

RemyDegenne committed 3 years ago

70b0e1dd

golf and docstrings

RemyDegenne committed 3 years ago

c29186de

chore(analysis/normed_space/extend): golf, add aux lemmas (#18927)

urkud committed 3 years ago

aa1dbeab

chore(*): removed unneeded imports (#18926)

kim-em committed 3 years ago

f0c8bf92

chore(ring_theory/kaehler): extract from `ring_theory/derivation` (#18935)

eric-wieser committed 3 years ago

73f96237

chore(analysis/inner_product_space/basic): golf, add/merge lemmas (#18928)

urkud committed 3 years ago

92c69b77

feat(measure_theory/constructions/prod): marginal measures (#18915)

RemyDegenne committed 3 years ago

726d2fe4

chore(ring_theory/discrete_valuation_ring): create folder ring_theory/discrete_valuation_ring (#18867)

faenuccio committed 3 years ago

c163ec99

feat(representation_theory/group_cohomology/basic): add standard definition of group cohomology (#18341)

Amelia Livingston committed 3 years ago

ef997baa

names, docstrings

RemyDegenne committed 3 years ago

7b8b3700

chore(data/set/intervals/monotone): fix names (#18924)

urkud committed 3 years ago

4d06b17a

chore(analysis/normed_space/basic): rename `abs_norm_eq_norm` to `abs_norm` (#18921)

urkud committed 3 years ago

f9dd3204

chore(data/{complex,is_R_or_C}/basic): fix name of `eq_conj_iff_*` lemmas (#18922)

eric-wieser committed 3 years ago

caa58cbf

feat(probability/kernel/composition): add a notation for the product of kernels (#18918)

RemyDegenne committed 3 years ago

15e02bcd

chore(ring_theory/polynomial/quotient): remove spurious restrict_scalars (#18916)

kim-em committed 3 years ago

61d8b824

refactor(algebra/order/to_interval_mod): Negate the definition of `mem_Ioo_mod` (#18912)

eric-wieser committed 3 years ago

645b6de4

feat(data/mv_polynomial/basic): add and generalize some lemmas from finsupp and monoid_algebra (#18855)

Hagb committed 3 years ago

f69db8ce

feat(analysis/special_functions): file for evaluations of specific improper integrals (#18821)

loefflerd committed 3 years ago

ec452806

feat(data/list/cycle): well-founded or transitive irreflexive relations don't have cycles (#18512)

vihdzp committed 3 years ago

7413128c

feat(algebra/algebra/basic): add shortcut instance (#18907)

Ruben-VandeVelde committed 3 years ago

36b8aa61

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

github-actions[bot] committed 3 years ago

ef553359

add kernel.comap_right and kernel.piecewise

RemyDegenne committed 3 years ago

817e6dbd

put basic kernel stuff into kernel.basic

RemyDegenne committed 3 years ago

01f4b0a9

golf, remove unused lemmas, etc.

RemyDegenne committed 3 years ago

20d5b6a8

feat(measure_theory/constructions/polish): a Polish Borel space is measurably equivalent to a subset of the reals (#18881)

Felix-Weilacher committed 3 years ago

11d5ff21

Merge remote-tracking branch 'origin/RD_aux3' into RD_disintegration

RemyDegenne committed 3 years ago

67dd53f8

Merge remote-tracking branch 'origin/RD_aux3' into RD_disintegration

RemyDegenne committed 3 years ago

85417aaa

minor. Where do I put those lemmas?

RemyDegenne committed 3 years ago

9025f8a9

RemyDegenne committed 3 years ago

0cd311ab

Newer Older