Commits leanprover-community/mathlib

WIP

TwoFX committed 3 years ago

398980db

refactor(category_theory/epi_mono): is_split_epi and split_epi (#16036)

joelriou committed 3 years ago

239d882c

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

leanprover-community-bot committed 3 years ago

b5b30b03

feat(probability/martingale/convergence): a.e. martingale convergence theorem (#15904)

kex-y committed 3 years ago

43e859a0

doc(ring_theory/valuation/valuation_subring): fix docstring (#16034)

kbuzzard committed 3 years ago

e1443c9c

feat(category_theory/preadditive/injective): Adjoint functors preserves injective objects (#15935)

jjaassoonn committed 3 years ago

0b8f638b

feat(algebra/module/bimodule): basic definitions for subbimodules (#14465)

ocfnash committed 3 years ago

58cef51f

feat(group_theory/group_action/defs): `vadd_assoc_class` (#15844)

YaelDillies committed 3 years ago

26e3eea8

refactor(*): Extend `×ˢ` notation (#15717)

YaelDillies committed 3 years ago

f1944b30

feat(category_theory/abelian): injective coseparator from separator and enough injectives (#15495)

TwoFX committed 3 years ago

24a55a05

feat(category_theory/localization): extension of natural transformations (#15747)

joelriou committed 3 years ago

fc739bf5

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

leanprover-community-bot committed 3 years ago

bd980416

chore(set_theory/ordinal/arithmetic): clean up `is_normal.sup` and related (#15162)

vihdzp committed 3 years ago

58d97787

feat(analysis/inner_product_space/l2_space): if `K` is a complete submodule then `E` is the Hilbert sum of `K` and `Kᗮ` (#15792)

ADedecker committed 3 years ago

8cfa8363

feat(geometry/manifold/complex): holomorphic functions are locally constant (#16015)

hrmacbeth committed 3 years ago

a9f99604

feat(ring_theory/roots_of_unity): generalisation linter (#16014)

ericrbg committed 3 years ago

de4a9ed1

feat(number_theory/cyclotomic/gal): generalise a little (#16012)

ericrbg committed 3 years ago

76fd4b2d

chore(number_theory/wilson): trivial strengthening (#16008)

ericrbg committed 3 years ago

c590a232

chore(data/polynomial/derivative): use 'nat_cast' rather than 'cast_nat' for consistency (#16005)

Ruben-VandeVelde committed 3 years ago

acae0c33

feat(algebra/order/sub): add `canonically_ordered_add_monoid.to_add_cancel_comm_monoid` (#15955)

eric-wieser committed 3 years ago

fc32854b

feat(data/fin/basic): coe_sub_iff_{le,lt} (#15930)

pechersky committed 3 years ago

eb5be8a0

fix(algebra/order/field_defs): move definitions to a separate file (#15783)

ericrbg committed 3 years ago

7dff8ed7

feat(ring_theory/adjoin_root): a bit of missing API for maps between certain quotients of `adjoin_root f` (#15757)

Paul-Lez committed 3 years ago

802513cb

feat(representation_theory/group_cohomology_resolution): show k[G^(n + 1)] is free over k[G] (#15501)

Amelia Livingston committed 3 years ago

811da369

feat(algebra/add_monoid_algebra/degree): new file with lemmas about support.sup/inf (#15413)

adomani committed 3 years ago

557f5e5d

feat(linear_algebra/span, matrix, finite_dimensional): new lemmas (#16006)

alreadydone committed 3 years ago

e2ba6de0

feat(topology/algebra/uniform_group): drop commutativity assumption in `topological_group.to_uniform_space` (#16004)

ocfnash committed 3 years ago

66b8fa75

feat(algebra/char_p): use `finite` instead of `fintype` (#16002)

urkud committed 3 years ago

2fae5fd7

feat(topology/separation): add `t0_space.of_cover` (#15982)

urkud committed 3 years ago

32a432cc

feat(ring_theory/algebraic): `alg_hom` from an algebraic extension to itself is bijective (#15873)

alreadydone committed 3 years ago

41cf8de0