Commits leanprover-community/mathlib3

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

RemyDegenne committed 2 years ago

15e02bcd

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

kim-em committed 2 years ago

61d8b824

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

eric-wieser committed 2 years ago

645b6de4

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

Hagb committed 2 years ago

f69db8ce

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

loefflerd committed 2 years ago

ec452806

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

vihdzp committed 2 years ago

7413128c

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

Ruben-VandeVelde committed 2 years ago

36b8aa61

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

leanprover-community-bot committed 2 years ago

ef553359

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

Felix-Weilacher committed 2 years ago

11d5ff21

chore(analysis/special_functions): Reduce imports in special_functions (#18909)

loefflerd committed 2 years ago

2c1d8ca2

chore(category_theory/monoidal/Mod): rename to Mod_ to avoid name clash in mathlib4 (#18911)

kim-em committed 2 years ago

33085c97

refactor(category_theory): removing additive_category (#18903)

joelriou committed 2 years ago

362c2263

refactor(number_theory/modular_forms/slash_actions): use the same notation everywhere (#18886)

eric-wieser committed 2 years ago

ef74e2bd

feat(ring_theory/norm): add norm_norm (#18860)

xroblot committed 2 years ago

fecd3520

feat(analysis/convex/cone/proper): define closure of a convex cone (#16335)

apurvnakade committed 2 years ago

620ba06c

chore(algebra/order/to_interval_mod): Reorder arguments (#18908)

YaelDillies committed 2 years ago

b2d7b50d

chore(category_theory/limits/preserves): fix typo (#18906)

kbuzzard committed 2 years ago

39478763

fix(algebra/module/submodule/basic): remove `submodule_class` (#18902)

eric-wieser committed 2 years ago

8130e515

chore(measure_theory/integral): split up measure_theory.integral.lebesgue (#18904)

loefflerd committed 2 years ago

7317149f

chore(.github/workflows): update gh-get-current-pr (#18763)

alexjbest committed 2 years ago

d20a8cd5

feat (measure_theory/integral): lemmas `integral_Ioi_eq_integral_Ici` etc (#18899)

loefflerd committed 2 years ago

8b8ba04e

chore(linear_algebra/matrix/to_linear_equiv): golf using existing morphisms (#18895)

eric-wieser committed 2 years ago

e42cfdb0

feat(analysis/fourier): Riemann-Lebesgue lemma (#17719)

loefflerd committed 2 years ago

9425b6f8

chore(data/finset/lattice): Move lemmas around (#18900)

YaelDillies committed 2 years ago

9d684a89

feat(ring_theory/ideal/quotient_operations): add double quotient of an algebra (#18452)

wupr committed 2 years ago

b88d81c8

feat(data/set/intervals/basic): generalize from `linear_order` to `preorder` (#18876)

eric-wieser committed 2 years ago

4367b192

feat(data/set/intervals/pi): `f.update i '' Icc a b = Icc (f.update i a) (f.update i b)` (#18892)

YaelDillies committed 2 years ago

e4bc74cb

chore (measure_theory/integral): split interval_integral.lean into two (#18898)

loefflerd committed 2 years ago

011cafb4

chore(.github/workflows): update get-changed-files and download-artifact version (#18765)

alexjbest committed 2 years ago

86d04064

chore(.github/workflows): update checkout and setup python versions (#18764)

alexjbest committed 2 years ago

7cc39182