Commits leanprover-community/mathlib3

Merge remote-tracking branch 'origin/master' into fourier-add-circle

hrmacbeth committed 3 years ago

88ea2c89

feat(measure_theory/integral/periodic): relate integrals over `add_circle` with integrals upstairs in `ℝ` (#16836)

hrmacbeth committed 3 years ago

f1138dc3

feat(topology/sets/closeds): atoms in a t1_space are singletons (#16721)

j-loreaux committed 3 years ago

2e348d40

chore(analysis/calculus/diff_ont_int_cont): rename to diff_cont_on_cl to match content (#16908)

sgouezel committed 3 years ago

8e9df645

feat(data/finset/basic): add instance `is_empty ↥∅` (#16902)

alreadydone committed 3 years ago

43a6243f

fix(number_theory/cyclotomic/basic): change variable names, fix doc (#16901)

jcommelin committed 3 years ago

ea3dac31

refactor(archive/100-theorems-list/02_cubing_a_cube): review API (#16898)

urkud committed 3 years ago

113568c9

feat(data/option/basic): add `option.{forall,exists}_mem_map` (#16897)

urkud committed 3 years ago

c5549d56

chore(*): remove uses of with_cases (#16894)

alexjbest committed 3 years ago

4d416710

feat(category_theory): yoneda functor on abelian category preserves finite colimits iff object is injective (#16893)

javra committed 3 years ago

8853975e

feat(algebraic_topology/dold_kan): very basic defs for split simplicial objects in preadditive categories (#16888)

joelriou committed 3 years ago

24f5150e

feat(ring_theory/ideal/local_ring): add local_ring.residue_field.map_id & local_ring.residue_field.map_comp (#16916)

mkaratarakis committed 3 years ago

bbcc67f5

feat(logic/equiv/transfer_instances, group_theory/eckmann_hilton): make definitions reducible (#16884)

alreadydone committed 3 years ago

2f93d81c

feat(topology/uniform_space): local uniform convergence on union (#16883)

b-mehta committed 3 years ago

a4efbb0e

feat(logic/basic): add four lemmas about (d)ite (#16879)

alreadydone committed 3 years ago

5fd24816

feat(data/real/ereal): `coe : ℝ → ereal` is strictly monotone (#16607)

YaelDillies committed 3 years ago

7507876b

feat(data/finset/basic): disj_Union (#16421)

eric-wieser committed 3 years ago

ccf8aa04

feat(data/set/intervals/unordered_interval): Intervals are injective in both endpoints (#16168)

YaelDillies committed 3 years ago

0a0be05e

feat(analysis/normed/ring/seminorm): Multiplicative ring norms (#16766)

YaelDillies committed 3 years ago

93def16e

feat(topology/uniform_space/basic): separation of compacts and closed sets in a uniform space (#16747)

ADedecker committed 3 years ago

300cf4dc

feat(data/option/basic): add `bind_some'` (#16641)

astrainfinita committed 3 years ago

f737ca11

feat(category_theory/groupoid/free): functoriality of the free groupoid plus some cleanup (#16907)

bottine committed 3 years ago

94fc87ee

feat(measure_theory/measure): add a measure_space instance for subtype (#16708)

alexjbest committed 3 years ago

695b3191

feat(analysis/locally_convex/with_seminorms): the topology induced by a family of seminorms is the infimum of the ones induced by each seminorm (#16669)

ADedecker committed 3 years ago

c80bc30e

feat(representation_theory/group_cohomology_resolution): add chain complex underlying the standard resolution (#16258)

Amelia Livingston committed 3 years ago

348289cc

perf(algebra/category/Module/monoidal): fix timeout (#16903)

alreadydone committed 3 years ago

556f3534

feat(category_theory): categories where inclusions into coproducts are mono (#16867)

joelriou committed 3 years ago

23d1b33c

chore(algebra/ring/basic): move results on dvd (#16864)

kim-em committed 3 years ago

b1aef433

feat(group_theory/subgroup/pointwise): Basic lemmas (#16856)

tb65536 committed 3 years ago

21926ffe

feat(ring_theory/etale): Formally unramified iff `Ω[S⁄R] = 0` (#16849)

erdOne committed 3 years ago

03eaefc4