leanprover-community/mathlib

Pull Requests Commits

awainverse committed 3 years ago

b15ecd11

feat(data/finset/pointwise): Missing operations (#12865)

YaelDillies committed 3 years ago

d5861954

feat(analysis/calculus): define `diff_on_int_cont` (#12688)

urkud committed 3 years ago

28eb06f9

feat(topology/order/hom/esakia): Esakia morphisms (#12241)

YaelDillies committed 3 years ago

5826b2fb

feat(algebra/big_operators/associated): generalize prod_primes_dvd (#12740)

Ruben-VandeVelde committed 3 years ago

41d291c7

refactor(measure_theory/integral): restrict interval integrals to real intervals (#12754)

urkud committed 3 years ago

3ce4161c

feat(combinatorics/simple_graph/inc_matrix): Incidence matrix (#10867)

YaelDillies committed 3 years ago

b0f585c5

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

leanprover-community-bot committed 3 years ago

01eb653d

feat(logic/basic): `ulift.down` is injective (#12824)

vihdzp committed 3 years ago

e51377fe

feat(topology/algebra/monoid): construct a unit from limits of units and their inverses (#12760)

j-loreaux committed 3 years ago

d71e06cc

feat(topology/continuous_function/units): basic results about units in `C(α, β)` (#12687)

j-loreaux committed 3 years ago

f9dc84ed

feat(category_theory/abelian): right derived functor (#12841)

jjaassoonn committed 3 years ago

8001ea54

feat(data/polynomial/eval + data/polynomial/ring_division): move a lemma and remove assumptions (#12854)

adomani committed 3 years ago

25ec622f

refactor(analysis/locally_convex/with_seminorms): use abbreviations to allow for dot notation (#12846)

mcdoll committed 3 years ago

fd4a034d

feat(model_theory/fraisse): Defines Fraïssé classes (#12817)

awainverse committed 3 years ago

a2e48025

feat(linear_algebra/span): generalize span_singleton_smul_eq (#12736)

eric-wieser committed 3 years ago

1b787d6b

docs(order/filter/basic): fix docstring of generate (#12734)

jcommelin committed 3 years ago

df299a19

feat(measure_theory/function/uniform_integrable): add API for uniform integrability in the probability sense (#12678)

kex-y committed 3 years ago

09750eb8

feat(model_theory/terms_and_formulas): Prenex Normal Form (#12558)

awainverse committed 3 years ago

715f984a

chore(order/{complete_lattice,sup_indep}): move `complete_lattice.independent` (#12588)

eric-wieser committed 3 years ago

091f27e8

feat(model_theory/definability): Definability lemmas (#12262)

awainverse committed 3 years ago

135c5742

split(data/{finset,set}/pointwise): Split off `algebra.pointwise` (#12831)

YaelDillies committed 3 years ago

86055c5d

feat(model_theory/ultraproducts): Ultraproducts and the Compactness Theorem (#12531)

awainverse committed 3 years ago

8161ba28

feat(measure_theory/constructions/borel_space): generalize a lemma (#12843)

urkud committed 3 years ago

8e9abe3c

chore(category/abelian/derived): shorten proof (#12847)

jjaassoonn committed 3 years ago

d902c222

feat(algebra/homology/additive): dualise statement of chain complex to cochain complex (#12840)

jjaassoonn committed 3 years ago

395019ee

feat(polynomial/derivative): tidy+new theorems (#12833)

ericrbg committed 3 years ago

69d3d16b

feat(order/compare): add 4 dot notation lemmas (#12832)

urkud committed 3 years ago

06017e07

chore(data/real/basic): tweak lemmas about `of_cauchy` (#12829)

eric-wieser committed 3 years ago

f5987b2a

feat(ring_theory/algebraic): Added basic lemmas + golf (#12820)

vihdzp committed 3 years ago

772c7766

Older