leanprover-community/mathlib

Pull Requests Commits

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

leanprover-community-bot committed 5 years ago

065bd5fc

style(combinatorics/simple_graph/basic): edit proof of lemma to match style guidelines (#5245)

agusakov committed 5 years ago

7e8e174b

feat(field_theory/galois): Is_galois iff is_galois bot (#5231)

tb65536 committed 5 years ago

ae99c76d

chore(data/multiset/basic): make `card` a bundled `add_monoid_hom` (#5228)

urkud committed 5 years ago

ddfba423

chore(data/equiv/ring): add `symm_symm` and `coe_symm_mk` (#5227)

urkud committed 5 years ago

1f648141

fix(topology/algebra/infinite_sum): fix docstring typos and add example (#5159)

kbuzzard committed 5 years ago

d4bd4cda

feat(category_theory/limits): morphisms to equalizer (#5233)

b-mehta committed 5 years ago

83b13d1c

chore(linear_algebra/basic): redefine `restrict` (#5229)

urkud committed 5 years ago

dd114987

chore(data/prod): `prod.swap` is `bijective` (#5226)

urkud committed 5 years ago

481f5e09

chore(data/equiv/basic): Add missing refl/trans/symm simp lemmas (#5223)

eric-wieser committed 5 years ago

c5009dd7

chore(category_theory/limits/preserves): make names consistent (#5240)

b-mehta committed 5 years ago

3972da8a

feat(order/filter/at_top_bot): `order_iso` maps `at_top` to `at_top` (#5236)

urkud committed 5 years ago

39a3b58b

chore(category_theory/limits): preserving coequalizers (#5212)

b-mehta committed 5 years ago

147a81a2

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

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

tb65536 committed 5 years ago

30467f4b

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

Newer Older