leanprover-community/mathlib

Pull Requests Commits

jcommelin committed 6 years ago

e95b15e9

Merge branch 'lean-3.4.2' into is-integrally-closed

jcommelin committed 6 years ago

d7992b79

feat(analysis/convex): interiors/closures of convex sets are convex in a tvs (#1781)

jlpaca committed 6 years ago

6bb17284

A `ring_exp` tactic for dealing with exponents in rings (#1715)

Vierkantor committed 6 years ago

5c093726

feat(tactic/default): import suggest (#1791)

robertylewis committed 6 years ago

1809eb40

feat(analysis/calculus/deriv): derivative of division and polynomials (#1769)

sgouezel committed 6 years ago

acd769af

(tactic/tidy): add docstring [skip ci] (#1788)

kbuzzard committed 6 years ago

4c382b12

feat(algebra/field_power): fpow is a strict mono (#1778)

jcommelin committed 6 years ago

3c9f8f0f

refactor(order/bounds,*): move code around to make `order.bounds` not depend on `complete_lattice` (#1783)

urkud committed 6 years ago

04559629

chore(travis): add instance priority linter to CI (#1787)

robertylewis committed 6 years ago

6968d749

feat(topology/subset_properties): fintype.compact_space (#1786)

jcommelin committed 6 years ago

8ca92637

feat(topology/dense_embedding): dense_range.equalizer (#1785)

jcommelin committed 6 years ago

70841824

feat(data/set/basic): more lemmas about `set.nonempty` (#1780)

urkud committed 6 years ago

7221900b

feat(data/set/finite): remove exists_finset_of_finite (#1782)

jcommelin committed 6 years ago

2adc122c

jcommelin committed 6 years ago

ea508fa6

feat(meta/expr): use structure_fields (#1766)

fpvandoorn committed 6 years ago

3e6fe842

Merge branch 'field-power-strict-mono' into is-integrally-closed

jcommelin committed 6 years ago

901644aa

Merge branch 'master' into field-power-strict-mono

jcommelin committed 6 years ago

Verified a847d98e

feat(algebra/field): remove is_field_hom (#1777)

jcommelin committed 6 years ago

de377ea3

feat(data/set/basic): define `set.nonempty` (#1779)

urkud committed 6 years ago

324ae4b1

fix(order.basic|ring_theory.algebra): lower instance priority (#1729)

fpvandoorn committed 6 years ago

d4ee5b69

doc(topology/basic): add a few doc strings [skip ci] (#1775)

urkud committed 6 years ago

43531676

feat(data/set/intervals): more properties of intervals (#1753)

sgouezel committed 6 years ago

c43b3329

Merge branch 'field-power-strict-mono' into is-integrally-closed

jcommelin committed 6 years ago

c1f0e354

Merge branch 'field-hom' into field-power-strict-mono

jcommelin committed 6 years ago

8feb6315

Fix up nolints.txt

jcommelin committed 6 years ago

85da1076

feat(data/nat/prime): monoid.prime_pow and docs (#1772)

jcommelin committed 6 years ago

2c2cbb0d

feat(algebra/field): remove is_field_hom

jcommelin committed 6 years ago

260d6533

jcommelin committed 6 years ago

720f231e

jcommelin committed 6 years ago

5b5bbca0

Older