leanprover-community/mathlib3

Pull Requests Commits

Merge remote-tracking branch 'origin/master' into eric-wieser/multilinear-tensor

eric-wieser committed 5 years ago

2a335040

refactor(*): drop `topology/instances/complex` (#5208)

urkud committed 5 years ago

c88e8f35

feat(ring_theory/witt_vector): common identities between operators on Witt vectors (#5161)

jcommelin committed 5 years ago

29a1731a

chore(*): clean up several unnecessary let statements (#5257)

alexjbest committed 5 years ago

339bd9a9

feat(data/polynomial): simp lemmas about polynomial derivatives (#5256)

alexjbest committed 5 years ago

12a8361f

chore(algebra/group_power): mark `map_pow` etc as `@[simp]` (#5253)

urkud committed 5 years ago

c6de6e4f

doc(data/list): fix `erasep` doc string (#5254)

robertylewis committed 5 years ago

85380712

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

Older