Commits leanprover-community/mathlib

feat(category_theory/limits): preserving pullbacks (#5668)

b-mehta committed 5 years ago

12945004

chore(linear_algebra/alternating): golf a proof (#5666)

eric-wieser committed 5 years ago

ce34ae6a

chore(algebra/group/hom): fix additive version of docstring (#5660)

jcommelin committed 5 years ago

0cd70d09

chore(analysis/special_functions/trigonometric): adding `@[pp_nodot]` to complex.log (#5670)

JamesAMaths committed 5 years ago

2b5344f5

feat(data/finset/intervals, data/set/intervals/basic): intersection of finset.Ico, union of intervals for sets and finsets (#5410)

RemyDegenne committed 5 years ago

aab5994e

feat(algebra/linear_ordered_comm_group_with_zero): Add linear_ordered_comm_monoid_with_zero and an instance for nat (#5645)

eric-wieser committed 5 years ago

d935760d

feat(geometry/manifold/times_cont_mdiff): API for checking `times_cont_mdiff` (#5631)

hrmacbeth committed 5 years ago

2bde21d1

feat(category_theory/closed): Frobenius reciprocity of cartesian closed categories (#5624)

b-mehta committed 5 years ago

bd9b03f6

feat(measure_theory/measure_space): ae_measurable and measurable are equivalent for complete measures (#5643)

RemyDegenne committed 5 years ago

0d7ca986

refactor(linear_algebra/alternating): Use unapplied maps when possible (#5648)

eric-wieser committed 5 years ago

9f066f1f

chore(algebra/ordered_monoid): rename lemmas (#5657)

fpvandoorn committed 5 years ago

795d5ab6

feat(measure_theory/borel_space): locally finite measure is sigma finite (#5634)

urkud committed 5 years ago

611bc865

refactor(algebra/module/basic): Clean up all the nat/int semimodule definitions (#5654)

eric-wieser committed 5 years ago

efdcab1a

feat(topology/algebra): add additive/multiplicative instances (#5662)

fpvandoorn committed 5 years ago

d89464d2

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

leanprover-community-bot committed 5 years ago

7500b242

feat(measure_theory): some additions (#5653)

fpvandoorn committed 5 years ago

4c3c8d78

chore(data/list/basic): tag mmap(') with simp (#5443)

pechersky committed 5 years ago

33a86cff

feat(category_theory/sites): category of sheaves on the trivial topology (#5651)

b-mehta committed 5 years ago

18ba69b7

feat(category_theory/monad): reflector preserves terminal object (#5649)

b-mehta committed 5 years ago

3c5d5c51

feat(measure_theory/borel_space): a compact set has finite measure (#5628)

urkud committed 5 years ago

a30c39e0

feat(category_theory/closed): golf definition and proofs (#5623)

b-mehta committed 5 years ago

4da83134

feat(category_theory/limits): the product comparison natural transformation (#5621)

b-mehta committed 5 years ago

fdbcab6a

feat(group_theory): add lemmas on solvability (#5646)

pglutz committed 5 years ago

2894260b

feat(docs/100): Add Masdeu's formalisation of Euler's Summation to 100.yaml (#5655)

jcommelin committed 5 years ago

66e02b35

feat(ring_theory/polynomial/cyclotomic): add cyclotomic.irreducible (#5642)

riccardobrasca committed 5 years ago

7bc2e9ef

feat(ring_theory/*): Various lemmas used to prove classical nullstellensatz (#5632)

dtumad committed 5 years ago

b9da50ad

feat(analysis/normed_space): affine map with findim domain is continuous (#5627)

urkud committed 5 years ago

3aea2845

chore(analysis/calculus): add `of_mem_nhds` versions of 2 lemmas (#5626)

urkud committed 5 years ago

833e9a04

feat(category_theory/limits): prod map is iso if components are (#5620)

b-mehta committed 5 years ago

e14d5eba

feat(linear_algebra/pi_tensor_product): define the tensor product of an indexed family of semimodules (#5311)

dupuisf committed 5 years ago

87ef7aff