leanprover-community/mathlib3

Pull Requests Commits

YaelDillies committed 3 years ago

32fac7b2

split files, fix lint

YaelDillies committed 3 years ago

fcc047bb

antoinelab01 committed 3 years ago

696aa3c6

add API for sums and prove sum_laplacian

antoinelab01 committed 3 years ago

5188957f

switch to multigraphs

YaelDillies committed 3 years ago

c270db18

YaelDillies committed 3 years ago

1c1b8e22

YaelDillies committed 3 years ago

eef80b1b

quotient by the kernel of the laplacian

YaelDillies committed 3 years ago

2dc24f48

YaelDillies committed 3 years ago

c7b842f3

feat(category_theory/limits): cone F ≌ costructured_arrow (const J) F (#15796)

TwoFX committed 3 years ago

8a032292

refactor(topology/constructions): review `quotient` API (#15986)

urkud committed 3 years ago

31800d81

refactor(category_theory/epi_mono): is_split_epi and split_epi (#16036)

joelriou committed 3 years ago

239d882c

chore(scripts): update nolints.txt (#16037)

leanprover-community-bot committed 3 years ago

b5b30b03

feat(probability/martingale/convergence): a.e. martingale convergence theorem (#15904)

kex-y committed 3 years ago

43e859a0

doc(ring_theory/valuation/valuation_subring): fix docstring (#16034)

kbuzzard committed 3 years ago

e1443c9c

feat(category_theory/preadditive/injective): Adjoint functors preserves injective objects (#15935)

jjaassoonn committed 3 years ago

0b8f638b

feat(algebra/module/bimodule): basic definitions for subbimodules (#14465)

ocfnash committed 3 years ago

58cef51f

feat(group_theory/group_action/defs): `vadd_assoc_class` (#15844)

YaelDillies committed 3 years ago

26e3eea8

refactor(*): Extend `×ˢ` notation (#15717)

YaelDillies committed 3 years ago

f1944b30

feat(category_theory/abelian): injective coseparator from separator and enough injectives (#15495)

TwoFX committed 3 years ago

24a55a05

feat(category_theory/localization): extension of natural transformations (#15747)

joelriou committed 3 years ago

fc739bf5

chore(scripts): update nolints.txt (#16020)

leanprover-community-bot committed 3 years ago

bd980416

chore(set_theory/ordinal/arithmetic): clean up `is_normal.sup` and related (#15162)

vihdzp committed 3 years ago

58d97787

feat(analysis/inner_product_space/l2_space): if `K` is a complete submodule then `E` is the Hilbert sum of `K` and `Kᗮ` (#15792)

ADedecker committed 3 years ago

8cfa8363

feat(geometry/manifold/complex): holomorphic functions are locally constant (#16015)

hrmacbeth committed 3 years ago

a9f99604

feat(ring_theory/roots_of_unity): generalisation linter (#16014)

ericrbg committed 3 years ago

de4a9ed1

feat(number_theory/cyclotomic/gal): generalise a little (#16012)

ericrbg committed 3 years ago

76fd4b2d

chore(number_theory/wilson): trivial strengthening (#16008)

ericrbg committed 3 years ago

c590a232

chore(data/polynomial/derivative): use 'nat_cast' rather than 'cast_nat' for consistency (#16005)

Ruben-VandeVelde committed 3 years ago

acae0c33

feat(algebra/order/sub): add `canonically_ordered_add_monoid.to_add_cancel_comm_monoid` (#15955)

eric-wieser committed 3 years ago

fc32854b

Older