leanprover-community/mathlib3

Pull Requests Commits

urkud committed 4 years ago

e4332a34

feat(group_theory/complement): `is_complement'.sup_eq_top` (#10230)

tb65536 committed 4 years ago

6cd63207

doc(README): add list of emeritus maintainers (#10288)

jcommelin committed 4 years ago

07be9042

feat(category_theory/sites/plus): `P⁺` for a presheaf `P`. (#10284)

adamtopaz committed 4 years ago

b51335c4

feat(measure_theory): define `measurable_space` instance on a quotient (#10275)

urkud committed 4 years ago

e6790930

chore(analysis/special_functions/pow): put lemmas about derivatives into a new file (#10153)

RemyDegenne committed 4 years ago

c45e70ac

refactor(linear_algebra/eigenspace): refactor `eigenvectors_linearly_independent` (#10198)

hrmacbeth committed 4 years ago

75207e91

feat(measure_theory/probability_mass_function): Define a measure assosiated to a pmf (#9966)

dtumad committed 4 years ago

1019dd67

feat(category_theory/sites/*): Dense subsite (#9694)

erdOne committed 4 years ago

9e1e4f01

chore(measure_theory): move `mutually_singular` to a new file (#10281)

urkud committed 4 years ago

6fd688b5

feat(category_theory/limits): Cone limiting iff terminal. (#10266)

erdOne committed 4 years ago

d7e320e6

feat(analysis/normed_space/star): introduce C*-algebras (#10145)

dupuisf committed 4 years ago

e5a79a7a

feat(field_theory/splitting_field): add eval_root_derivative_of_split (#10224)

riccardobrasca committed 4 years ago

d6056eee

feat(category_theory/limits/concrete_category): A lemma about concrete multiequalizers (#10277)

adamtopaz committed 4 years ago

73b2b651

feat(field_theory/separable): X^n - 1 is separable iff ↑n ≠ 0. (#9779)

ericrbg committed 4 years ago

0b4c5409

chore(category_theory/isomorphisms): Adjust priority for is_iso.comp_is_iso (#10276)

adamtopaz committed 4 years ago

8cd5f0ee

feat(linear_algebra/pi_tensor_product): add subsingleton_equiv (#10274)

eric-wieser committed 4 years ago

d6860258

feat(measure_theory): integral over a family of pairwise a.e. disjoint sets (#10268)

urkud committed 4 years ago

f99d6386

refactor(group_theory/complement): Generalize `card_mul` to from subgroups to subsets (#10264)

tb65536 committed 4 years ago

12c868a5

feat(linear_algebra/pi_tensor_prod): generalize actions and provide missing smul_comm_class and is_scalar_tower instance (#10262)

eric-wieser committed 4 years ago

72ca0d33

feat(group_theory/submonoid/membership): `exists_multiset_of_mem_closure` (#10256)

tb65536 committed 4 years ago

c7f3e5c6

feat(data/finset/pairwise): Interaction of `set.pairwise_disjoint` with `finset` (#10244)

YaelDillies committed 4 years ago

9a30dcfd

feat(group_theory/index): Index of `subgroup.map` (#10232)

tb65536 committed 4 years ago

820f8d72

feat(algebra/order/sub): An `add_group` has ordered subtraction (#10225)

YaelDillies committed 4 years ago

4b1a0577

feat(data/polynomial): assorted lemmas on division and gcd of polynomials (#9600)

Vierkantor committed 4 years ago

a9c3ab5d

feat(analysis/subadditive): prove that, if u_n is subadditive, then u_n / n converges. (#10258)

sgouezel committed 4 years ago

01e7b209

chore(analysis/special_functions/complex/log): move results about derivatives to a new file (#10117)

RemyDegenne committed 4 years ago

4df3cd76

chore(probability_theory/notation): change `volume` to `measure_theory.measure.volume` (#10272)

kex-y committed 4 years ago

6e268cd8

feat(measure_theory): add `ae_measurable.sum_measure` (#10271)

urkud committed 4 years ago

270c644c

feat(*): more bundled versions of `(fin 2 → α) ≃ (α × α)` (#10214)

urkud committed 4 years ago

c062d9ea

Older