leanprover-community/mathlib

Pull Requests Commits

refactor(combinatorics/simple_graph/matching): change definition of matching (#5210)

agusakov committed 5 years ago

b82eb7a5

feat(analysis): define asymptotic equivalence of two functions (#4979)

ADedecker committed 5 years ago

dc08f4d4

feat(algebra/group): composition of monoid homs as "bilinear" monoid hom (#5202)

jcommelin committed 5 years ago

de7dbbbd

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

leanprover-community-bot committed 5 years ago

56c4e732

chore(data/finsupp/basic): Add single_of_single_apply (#5219)

eric-wieser committed 5 years ago

0afd3a0f

feat(dynamics): (semi-)flows, omega limits (#4843)

jlpaca committed 5 years ago

8a9a5d35

doc(data/quot): Fix typo (#5221)

eric-wieser committed 5 years ago

5f430798

chore(algebra/big_operators/basic): Split prod_cancels_of_partition_cancels in two and add a docstring (#5218)

eric-wieser committed 5 years ago

4ea2e68d

feat(linear_algebra/multilinear): Add `multilinear_map.coprod` (#5182)

eric-wieser committed 5 years ago

5ea96f9a

feat(ring_theory/discrete_valuation_ring): add additive valuation (#5094)

kbuzzard committed 5 years ago

cb7effa8

doc(data/typevec): Fix broken markdown rendering (#5220)

eric-wieser committed 5 years ago

f1d30f6e

docs(data/fp): Move title comment so that it appears in the markdown (#5222)

eric-wieser committed 5 years ago

54c13bd8

Update `refine_struct` test

Vierkantor committed 5 years ago

06313d53

feat(field_theory/adjoin): induction on adjoin (#5173)

tb65536 committed 5 years ago

30467f4b

Use `sub_eq_add_neg` instead of `dunfold` to rewrite `a - b` to `a + -b`

Vierkantor committed 5 years ago

45c4df61

Merge remote-tracking branch 'mathlib/master' into bundle_has_sub_div

Vierkantor committed 5 years ago

7825287d

chore(algebra/ring): delete a duplicate instance (#5215)

alexjbest committed 5 years ago

7e307bcc

feat(category_theory/limits): cleanup equalizers (#5214)

b-mehta committed 5 years ago

2d00ba48

feat(category_theory/limits): reflects limit if reflects iso and preserves (#5213)

b-mehta committed 5 years ago

b2f8c4c0

chore(topology/continuous_on): change type of `continuous_on.comp_continuous` (#5209)

urkud committed 5 years ago

cfd01f9d

refactor(data/polynomial/derivative): change `polynomial.derivative` to be a `linear_map` (#5198)

awainverse committed 5 years ago

ad25cacf

feat(category_theory/monad): cleanups in monad algebra (#5193)

b-mehta committed 5 years ago

240f6eb9

feat(ring_theory/polynomial/cyclotomic): add order_of_root_cyclotomic (#5151)

riccardobrasca committed 5 years ago

c10d1b1f

feat(category_theory/limits/preserves): preserving terminal objects (#5060)

b-mehta committed 5 years ago

c939c9e4

feat(ring_theory/polynomial/cyclotomic): Möbius inversion formula for cyclotomic polynomials (#5192)

awainverse committed 5 years ago

4f5046dd

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

leanprover-community-bot committed 5 years ago

57dd302d

feat(algebra/lie/basic): define missing inclusion maps (#5207)

Oliver Nash committed 5 years ago

20cc59d9

feat(topology/algebra/order): continuity of monotone functions (#5199)

urkud committed 5 years ago

ec839ef0

doc(tactic/library_search): use more detailed doc string in docs (#5206)

robertylewis committed 5 years ago

3894503e

feat(topology/category/Profinite): add category of profinite top. spaces (#5147)

kbuzzard committed 5 years ago

d416ad69

Newer Older