Commits leanprover-community/mathlib

fix

eric-wieser committed 3 years ago

97927e03

more norm_cast

eric-wieser committed 3 years ago

e86bd2b6

chore(*): add some missing `norm_cast` attributes

eric-wieser committed 3 years ago

3760eeb4

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

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

tb65536 committed 3 years ago

45ef183d

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

hrmacbeth committed 3 years ago

0fbd703b

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

urkud committed 3 years ago

43e95eef

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

ReimannJ committed 3 years ago

7bbc52b7

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

jsm28 committed 3 years ago

34c70db6

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

jsm28 committed 3 years ago

abed0373

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

jsm28 committed 3 years ago

069c3d1e

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

urkud committed 3 years ago

c8243a6a

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

jsm28 committed 3 years ago

419c83f6

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

kim-em committed 3 years ago

3348bed9

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

sgouezel committed 3 years ago

476f28f8

feat(analysis/calculus): bounded variation functions (#16683)

sgouezel committed 3 years ago

aadde303

feat(algebra/algebra/basic): make algebra_map a low prio has_lift_t (#16567)

kbuzzard committed 3 years ago

d840349d

feat(ring_theory/valuation): Equivalent conditions of DVRs. (#15081)

erdOne committed 3 years ago

10a3d03b

refactor(analysis/normed_space/spectrum): remove `norm_one_class` hypotheses (#16891)

j-loreaux committed 3 years ago

71a08c30

chore(ring_theory.dedekind_domain.adic_valuation): delete outdated comment (#16886)

mariainesdff committed 3 years ago

d20f598e

feat(topology/algebra/group): discrete subgroup acts properly discontinuously (#16593)

hrmacbeth committed 3 years ago

c476f200

fix(.github/CODEOWNERS): disable catch-all pattern for now (#16892)

jcommelin committed 3 years ago

fbfef5a1