Commits leanprover-community/mathlib

add file containing the Weierstrass M-test

CBirkbeck committed 4 years ago

34761ea6

feat(analysis/complex/basic): convex_on.sup (#8958)

pechersky committed 4 years ago

5e27f509

feat(algebra/ordered_ring): `linear_ordered_semiring` extends `linear_ordered_add_comm_monoid` (#8961)

pechersky committed 4 years ago

fdc24f53

feat(group_theory/group_action/basic): class formula, Burnside's lemma (#8801)

ADedecker committed 4 years ago

d821860f

feat(number_theory): define number fields, function fields and their rings of integers (#8701)

Vierkantor committed 4 years ago

17747c09

feat(ring_theory/ideal): generalize from `integral_closure` to `is_integral_closure` (#8944)

Vierkantor committed 4 years ago

88525a98

feat(group_theory/coset): rw lemmas involving quotient_group.mk (#8957)

tb65536 committed 4 years ago

55a7d385

fix(group_theory/group_action/defs): deduplicate `const_smul_hom` and `distrib_mul_action.to_add_monoid_hom` (#8953)

eric-wieser committed 4 years ago

baefdf34

feat(algebra/group/hom_instance): additive endomorphisms form a ring (#8954)

eric-wieser committed 4 years ago

1dddd7f9

refactor(*): rename {topological,smooth}_semiring to {topological,smooth}_ring (#8902)

jcommelin committed 4 years ago

2fa82513

feat(category_theory/limits/kan_extension): Prove (co)reflectivity for Kan extensions (#8962)

adamtopaz committed 4 years ago

289e6dc6

chore(analysis/convex/basic): generalize `concave_on.le_on_segment` to monoids (#8959)

pechersky committed 4 years ago

8da6699f

feat(ring_theory/dedekind_domain): the integral closure of a DD is a DD (#8847)

Vierkantor committed 4 years ago

9d3e3e8a

feat(order/bounded_lattice): `ne_(bot|top)_iff_exists` (#8960)

pechersky committed 4 years ago

6c247315

feat(group_theory): Add `monoid_hom.mker` and generalise the codomain for `monoid_hom.ker` (#8532)

shingtaklam1324 committed 4 years ago

07c57b56

feat(tactic/lint): minor linter improvements (#8934)

fpvandoorn committed 4 years ago

0b8a858f

chore(algebra,group_theory,right_theory,linear_algebra): add missing lemmas (#8948)

eric-wieser committed 4 years ago

9b000466

fix(category_theory/adjunction/basic): Fix typo in docstring (#8950)

justus-springer committed 4 years ago

2beaa28a

feat(topology/algebra/localization): add topological localization (#8894)

mariainesdff committed 4 years ago

510e65d7

feat(order/basic): recursor for order_dual (#8938)

pechersky committed 4 years ago

d472e1bd

feat(order/well_founded): define `function.argmin`, `function.argmin_on` (#8895)

ocfnash committed 4 years ago

0970d07d

feat(order/bounded_lattice): unbot and untop (#8885)

pechersky committed 4 years ago

faf5e5c9

feat(group_theory/perm/basic): permutations of a subtype (#8691)

YaelDillies committed 4 years ago

f3101e82

feat(algebraic_geometry): Redefine Schemes in terms of isos of locally ringed spaces (#8888)

justus-springer committed 4 years ago

73f50ac6

feat(measure_theory/conditional_expectation): the integral of the norm of the conditional expectation is lower (#8318)

RemyDegenne committed 4 years ago

5b04a896

feat(algebra/group/defs): ext lemmas for (semi)groups and monoids (#8391)

bryangingechen committed 4 years ago

f0451d80

feat(algebra/{pointwise,algebra/operations}): add `supr_mul` and `mul_supr` (#8923)

alexjbest committed 4 years ago

065a35dc

feat(algebra/{module/linear_map, algebra/basic}): Add `distrib_mul_action.to_linear_(map|equiv)` and `mul_semiring_action.to_alg_(hom|equiv)` (#8936)

eric-wieser committed 4 years ago

93390069

chore(order/bounded_lattice): dot-notation lemmas ne.bot_lt and ne.lt_top (#8935)

jcommelin committed 4 years ago

3d6a8285

chore(topology/metric_space/basic): add `metric.uniform_continuous_on_iff_le` (#8906)

urkud committed 4 years ago

12bbd533