Commits leanprover-community/mathlib

Prove Dirichlet's test for complex sequences

ecstatic-morse committed 3 years ago

1370b7fe

feat(algebra/big_operators/intervals): summation by parts

ecstatic-morse committed 3 years ago

7a88b2b7

chore(measure_theory/integral/lebesgue): use to_additive when declaring instances and basic lemmas about simple functions (#12000)

RemyDegenne committed 3 years ago

af1355c4

chore(topology/algebra): rename file to match renamed lemmas (#11996)

eric-wieser committed 3 years ago

4b217ea7

chore(data/finset/basic): Golf and compress (#11987)

YaelDillies committed 3 years ago

4a4a3a90

chore(measure_theory/function/ae_eq_fun): replace topological assumptions by measurability assumptions (#11981)

RemyDegenne committed 3 years ago

5f70cd95

feat(group_theory/sylow): all max groups normal imply sylow normal (#11841)

nomeata committed 3 years ago

b72300f3

feat(analysis/analytic/basic): add uniqueness results for power series (#11896)

j-loreaux committed 3 years ago

06e7f767

feat(order/category/BoundedOrder): The category of bounded orders (#11961)

YaelDillies committed 3 years ago

91cc4ae6

chore(topology/algebra/ordered/*): Rename folder (#11988)

YaelDillies committed 3 years ago

1b5f8c28

chore(category_theory/monad/equiv_mon): Removing some slow uses of `obviously` (#11980)

stuart-presnell committed 3 years ago

7bebee66

chore(topology/algebra/module/multilinear): relax typeclass arguments (#11972)

eric-wieser committed 3 years ago

71e90063

refactor(measure_theory/group/basic): rename and split (#11952)

fpvandoorn committed 3 years ago

822244f7

feat(topology/instances/real): metric space structure on nat (#11963)

sgouezel committed 3 years ago

60d32337

feat(tactic/lint): add unprintable tactic linter (#11725)

digama0 committed 3 years ago

dff8393c

feat(category_theory/category/Twop): The category of two-pointed types (#11844)

YaelDillies committed 3 years ago

227293b5

chore(order/cover): Rename `covers` to `covby` (#11984)

YaelDillies committed 3 years ago

788240cf

doc(data/finset/basic): correct some function names (#11983)

kmill committed 3 years ago

3fcb7380

refactor(data/nat/factorization): Use factorization instead of factors.count (#11384)

b-mehta committed 3 years ago

515ce797

feat(measure_theory/measure/haar_quotient): Pushforward of Haar measure is Haar (#11593)

AlexKontorovich committed 3 years ago

da76d218

feat(number_theory/number_field/basic) : the ring of integers of a number field is not a field (#11956)

mariainesdff committed 3 years ago

edefc116

feat(measure_theory/function/ae_eq_of_integral): remove a few unnecessary `@` (#11974)

RemyDegenne committed 3 years ago

1b78b4d1

fix(algebra/monoid_algebra/basic): remove an instance that forms a diamond (#11918)

eric-wieser committed 3 years ago

114752ca

feat(model_theory/direct_limit): Direct limits of first-order structures (#11789)

awainverse committed 3 years ago

492393b0

feat(data/pi): provide `pi.mul_single` (#11849)

nomeata committed 3 years ago

024aef0b

fix(ring_theory/algebraic): prove a diamond exists and remove the instances (#11935)

eric-wieser committed 3 years ago

8c60a927

chore(data/real/ennreal, topology/instances/ennreal): change name of the order isomorphism for `inv` (#11959)

j-loreaux committed 3 years ago

fbfdff7e

chore(algebra/star): generalize star_bit0, add star_inv_of (#11951)

eric-wieser committed 3 years ago

ae14f6ad

feat(topology/algebra/group): added (right/left)_coset_(open/closed) (#11876)

Sebastian-Monnet committed 3 years ago

0227820c

refactor(order/well_founded, set_theory/ordinal_arithmetic): Fix namespace in `self_le_of_strict_mono` (#11871)

vihdzp committed 3 years ago

73513580