leanprover-community/mathlib

Pull Requests Commits

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

eric-wieser committed 4 years ago

ccf8aa04

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

YaelDillies committed 4 years ago

0a0be05e

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

YaelDillies committed 4 years ago

93def16e

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

ADedecker committed 4 years ago

300cf4dc

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

astrainfinita committed 4 years ago

f737ca11

Add instance for T1 space

Multramate committed 4 years ago

6167a481

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

bottine committed 4 years ago

94fc87ee

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

alexjbest committed 4 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 4 years ago

c80bc30e

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

Amelia Livingston committed 4 years ago

348289cc

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

alreadydone committed 4 years ago

556f3534

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

joelriou committed 4 years ago

23d1b33c

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

kim-em committed 4 years ago

b1aef433

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

tb65536 committed 4 years ago

21926ffe

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

erdOne committed 4 years ago

03eaefc4

feat(group_theory/subgroup/basic): The center can be written as the intersection of centralizers (#16837)

tb65536 committed 4 years ago

45ef183d

feat(topology/instances/add_circle): the additive circle `ℝ / (a ∙ ℤ)` is normal (T4) and second-countable (#16594)

hrmacbeth committed 4 years ago

0fbd703b

feat(topology/separation): add instances about `separation_quotient` (#16579)

urkud committed 4 years ago

43e95eef

feat(measure_theory/integral/riesz_markov_kakutani): begin construction of content for Riesz-Markov-Kakutani (#16367)

ReimannJ committed 4 years ago

7bbc52b7

Replace as_ideal with to_ideal

Multramate committed 4 years ago

6f508023

Revert style changes

Multramate committed 4 years ago

c55cad14

Add equivalence between maximal and height one spectra

Multramate committed 4 years ago

eda4ce9e

Define maximal spectrum

Multramate committed 4 years ago

3f3de3cb

feat(geometry/euclidean/oriented_angle): oriented angles and betweenness (#16824)

jsm28 committed 4 years ago

34c70db6

feat(geometry/euclidean/oriented_angle): collinearity and affine independence (#16822)

jsm28 committed 4 years ago

abed0373

feat(linear_algebra/affine_space/independent): affine independence of all but one point (#16815)

jsm28 committed 4 years ago

069c3d1e

feat(group_theory/submonoid/basic): add `monoid_hom.of_mclosure_eq_top_left` (#16809)

urkud committed 4 years ago

c8243a6a

feat(linear_algebra/affine_space/finite_dimensional): more `collinear` lemmas (#16806)

jsm28 committed 4 years ago

419c83f6

chore(tactic/linarith): remove unneeded code (#16791)

kim-em committed 4 years ago

3348bed9

feat(analysis/analytic/uniqueness): two analytic functions that coincide locally coincide globally (#16723)

sgouezel committed 4 years ago

476f28f8

Newer Older