leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' of github.com:leanprover-community/mathlib into eric-wieser/alternating_map_product-tmul-int

eric-wieser committed 4 years ago

9c1797a1

eric-wieser committed 4 years ago

0abcb4b5

fix(*): Tidy up the finset helpers

eric-wieser committed 4 years ago

fd704f30

Extract a helper lemma

eric-wieser committed 4 years ago

de32fd26

All working again

eric-wieser committed 4 years ago

b2d88fef

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

eric-wieser committed 4 years ago

9f066f1f

eric-wieser committed 4 years ago

0863877b

Try for an `ext v`-free proof

eric-wieser committed 4 years ago

8b8b220b

Only the last proof is still broken

eric-wieser committed 4 years ago

cb4d021a

eric-wieser committed 4 years ago

b6d34cf8

Merge branch 'eric-wieser/alternating-map-smul' into eric-wieser/alternating_map_product-tmul-int

eric-wieser committed 4 years ago

1f69e8d7

feat(*): Make comp_alternating_map an add_monoid_hom

eric-wieser committed 4 years ago

e4bd5ee0

Diamond problem is gone!

eric-wieser committed 4 years ago

77129217

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

fpvandoorn committed 4 years ago

795d5ab6

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

eric-wieser committed 4 years ago

b4ac6fdf

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

urkud committed 4 years ago

611bc865

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

eric-wieser committed 4 years ago

efdcab1a

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

fpvandoorn committed 4 years ago

d89464d2

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

leanprover-community-bot committed 4 years ago

7500b242

feat(measure_theory): some additions (#5653)

fpvandoorn committed 4 years ago

4c3c8d78

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

pechersky committed 4 years ago

33a86cff

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

b-mehta committed 4 years ago

18ba69b7

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

b-mehta committed 4 years ago

3c5d5c51

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

urkud committed 4 years ago

a30c39e0

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

b-mehta committed 4 years ago

4da83134

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

b-mehta committed 4 years ago

fdbcab6a

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

pglutz committed 4 years ago

2894260b

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

jcommelin committed 4 years ago

66e02b35

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

riccardobrasca committed 4 years ago

7bc2e9ef

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

dtumad committed 4 years ago

b9da50ad

Older