leanprover-community/mathlib

Pull Requests Commits

fix(tactic/solve_by_elim): parameter parsing (#1591)

kim-em committed 6 years ago

5da754c9

chore(*): pass dup_namespace and def_lemma lint tests (#1599)

robertylewis committed 6 years ago

4b9cdf44

feat(data/multiset): map_eq_map_of_bij_of_nodup (#1590)

ChrisHughes24 committed 6 years ago

31c73c1d

feat(algebra/semiconj): define `semiconj_by` and some operations (#1576)

urkud committed 6 years ago

08977be6

feat(geometry/manifold): improvements for smooth manifolds (#1593)

sgouezel committed 6 years ago

e2a8e639

feat(algebra/big_operators): sum_ite (#1598)

ChrisHughes24 committed 6 years ago

b433afa7

doc(topology/topological_fiber_bundle): documentation improvements (#1594)

sgouezel committed 6 years ago

36dfcfcd

feat(data/nat/modeq): div_mod_eq_mod_mul_div (#1597)

ChrisHughes24 committed 6 years ago

d214c61c

fix(suggest): focus1 at the correct moment (#1592)

kim-em committed 6 years ago

36f71138

chore(src/data/mv_polynomial): doc comments and removing unused arguments (#1585)

kim-em committed 6 years ago

24dd80b0

feat(analysis/normed_space): norms on ℤ and ℚ (#1570)

urkud committed 6 years ago

079e6ec9

fix(category_theory/adjunctions): fix deterministic timeouts (#1586)

kim-em committed 6 years ago

ee5518c2

refactor(data/finset): restate disjoint_filter (#1583)

ChrisHughes24 committed 6 years ago

5722ee88

chore(algebra/category/CommRing/limits): fix typo, remove private (#1584)

kim-em committed 6 years ago

31906d88

feat(algebra/group): conversion between `→*` and `→+` (#1569)

urkud committed 6 years ago

e8bdb05e

feat(archive): add proof of sensitivity conjecture (#1553)

robertylewis committed 6 years ago

93b17864

chore(algebra/category/*/colimits): remove unnecessary projections (#1588)

kim-em committed 6 years ago

1b4d1eaa

feat(category_theory): add `reassoc` annotations (#1558)

cipher1024 committed 6 years ago

2b98d47a

feat(data/nat/basic): division inequalities (#1579)

ChrisHughes24 committed 6 years ago

1741a1d6

refactor(category_theory,algebra/category): make algebraic categories not [reducible] (#1491)

rwbarton committed 6 years ago

c9ba7a5c

feat(data/finset): inj_on_of_surj_on_of_card_le (#1578)

ChrisHughes24 committed 6 years ago

340178d8

feat(*): various lemmas from the sensitivity project (#1550)

robertylewis committed 6 years ago

39092ab0

docs(README): Remove Patrick from the maintainer list.

PatrickMassot committed 6 years ago

96ebf8cc

fix(algebra/group/hom): Fix spurrious arguments (#1581)

PatrickMassot committed 6 years ago

6cf3d040

feat(geometric/manifold): smooth manifolds (#1555)

sgouezel committed 6 years ago

f19dbf29

feat(data/finset): define `finset.Ico.subset_iff` (#1574)

urkud committed 6 years ago

f52e952e

feat(topology/topological_fiber_bundle): topological fiber bundles (#1421)

sgouezel committed 6 years ago

a4bbbdea

feat(algebra/geom_sum): sum of a geom_series over an Ico (#1573)

urkud committed 6 years ago

d2d29ffd

fix(scripts): sanity_check -> lint [ci skip] (#1575)

fpvandoorn committed 6 years ago

0b660a9f

feat(topology/metric_space): polygonal version of the triangle inequality (#1572)

urkud committed 6 years ago

809276c0

Newer Older