leanprover-community/mathlib

Pull Requests Commits

urkud committed 5 years ago

9abe1357

chore(order/filter/bases): golf a proof (#4834)

urkud committed 5 years ago

2283cf06

Merge branch 'nested-intervals' into cauchy-rect

urkud committed 5 years ago

34657391

Merge commit 'b01addfb8' into cauchy-rect

urkud committed 5 years ago

4e28f6fb

Docs, two more versions

urkud committed 5 years ago

0b8d6dfe

urkud committed 5 years ago

b01addfb

urkud committed 5 years ago

4cc590d2

feat(algebra/module/ordered): add pi instance

urkud committed 5 years ago

5d02a270

Revert some changes

urkud committed 5 years ago

d103fe19

urkud committed 5 years ago

06c3ecea

Merge branch 'extra-classes' into cauchy-rect

urkud committed 5 years ago

5e4536a9

Merge commit '16256cf9a' into cauchy-rect

urkud committed 5 years ago

3bd46f46

urkud committed 5 years ago

547a1931

feat(analysis/calculus/times_cont_diff): differentiability of field inverse (#4795)

urkud committed 5 years ago

94fa9058

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

leanprover-community-bot committed 5 years ago

d5650a7f

Ennreal instance

urkud committed 5 years ago

6cb353d6

feat(data/polynomial/lifts): polynomials that lift (#4796)

riccardobrasca committed 5 years ago

cc7f06bd

feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero (#4766)

eric-wieser committed 5 years ago

bfadf057

urkud committed 5 years ago

77951f9c

urkud committed 5 years ago

16256cf9

Merge branch 'master' into cauchy-rect

urkud committed 5 years ago

561256fb

urkud committed 5 years ago

973e8a3d

feat(number_theory/fermat4): The n=4 case of fermat (#4720)

paulvanwamelen committed 5 years ago

58f8817e

feat(ring_theory/witt_vector/is_poly): supporting ghost calculations (#4691)

jcommelin committed 5 years ago

d28e3d10

feat(field_theory/intermediate_field): equalities from inclusions and dimension bounds (#4828)

tb65536 committed 5 years ago

3aac0287

feat(data/polynomial): ext lemmas for homomorphisms from `polynomial R` (#4823)

urkud committed 5 years ago

6ec7aece

feat(data/dfinsupp): Port over the `finsupp.lift_add_hom` API (#4821)

eric-wieser committed 5 years ago

03a477c4

feat(data/equiv, algebra/*): Add simps projections to many equivs and homs (#4818)

eric-wieser committed 5 years ago

5ae192eb

chore(topology/basic): the set of cluster pts of a filter is a closed set (#4815)

urkud committed 5 years ago

d46d0c27

chore(data/dfinsupp): Provide dfinsupp with a semimodule instance (#4801)

eric-wieser committed 5 years ago

072cfc55

Newer Older