Commits leanprover-community/mathlib

refactor(data/polynomial): Move some lemmas to `monoid_algebra` (#4627)

eric-wieser committed 5 years ago

46b0528b

feat(algebra/category/Algebra/basic): Add free/forget adjunction. (#4620)

adamtopaz committed 5 years ago

abaf3c29

feat(algebra/algebra/basic): Add `map_finsupp_(sum|prod)` to `alg_(hom|equiv)` (#4603)

eric-wieser committed 5 years ago

07ee11e7

feat(algebra/gcd_monoid): in a gcd_domain a coprime factor of a power is a power (#4589)

paulvanwamelen committed 5 years ago

bb1f5492

feat(data/matrix/notation): simp lemmas for constant-indexed elements (#4491)

jsm28 committed 5 years ago

b01ca810

feat(data/polynomial/eval): bit0_comp, bit1_comp (#4617)

jcommelin committed 5 years ago

85d4b574

fix(haar_measure): minor changes (#4623)

fpvandoorn committed 5 years ago

1444fa52

lint(data/num/*): add docs and remove some [has_zero] requirements (#4604)

ADedecker committed 5 years ago

7559d1c8

chore(category_theory/monoidal): fix typo in docstrings (#4625)

jcommelin committed 5 years ago

fa652828

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

leanprover-community-bot committed 5 years ago

2e1129eb

chore(algebra/order,data/set/intervals): a few more trivial lemmas (#4611)

urkud committed 5 years ago

084b7e7d

fix(tactic/suggest): properly remove "Try this: exact " prefix from library_search hole command (#4609)

bryangingechen committed 5 years ago

d11eb847

doc(category_theory/comma): Fix markdown rendering in docs (#4618)

eric-wieser committed 5 years ago

40844f01

feat(data/set/intervals): more lemmas about `unordered_interval` (#4607)

urkud committed 5 years ago

de463493

feat(linear_algebra/clifford_algebra): Add a definition derived from exterior_algebra.lean (#4430)

eric-wieser committed 5 years ago

442ef226

doc(docs/100): link to actual triangle inequality (#4614)

gebner committed 5 years ago

Verified 1a1655c0

feat(algebra/char_zero): char_zero.infinite (#4593)

jcommelin committed 5 years ago

f7edbca4

chore(linear_algebra/linear_independent): review API (#4567)

urkud committed 5 years ago

6f5ccc1e

refactor(data/int/gcd,ring_theory/int/basic): collect integer divisibility results from various files (#4572)

paulvanwamelen committed 5 years ago

85117294

feat(data/polynomial/field_division, field_theory/splitting_field): Splits if enough roots (#4557)

riccardobrasca committed 5 years ago

20006f10

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

leanprover-community-bot committed 5 years ago

1c12bd95

feat(analysis/normed_space): unconditionally convergent series in `R^n` is absolutely convergent (#4551)

urkud committed 5 years ago

e2dd1c67

refactor(*): migrate to `dense` API (#4447)

urkud committed 5 years ago

2543b688

chore(multiset): dedicated notation for multiset.cons (#4600)

jcommelin committed 5 years ago

fde3d78c

chore(number_theory/arithmetic_function): Define in terms of zero_hom (#4606)

eric-wieser committed 5 years ago

7368d719

feat(analysis/normed_space/operator_norm): construct a continuous_linear_equiv from a linear_equiv and bounds in both directions (#4583)

dupuisf committed 5 years ago

b1c1033f

feat(data/vector2): induction principle, define last, and some lemmas (blocked by #4578) (#4554)

pechersky committed 5 years ago

7cff8250

chore(linear_algebra/finsupp): Implement lsingle in terms of single_add_hom (#4605)

eric-wieser committed 5 years ago

71bb9f23

chore(algebra/monoid_algebra): Replace `algebra_map'` with `single_(zero|one)_ring_hom` (#4582)

eric-wieser committed 5 years ago

ca6af1c4

feat(algebra/char_p): fields with a hom between them have same char (#4594)

jcommelin committed 5 years ago

9f9344d3