leanprover-community/mathlib

Pull Requests Commits

feat(ring_theory/power_series): inverse lemmas (#4552)

b-mehta committed 5 years ago

d533e1ce

feat(topology/basic): Lim_spec etc. cleanup (#4545)

adamtopaz committed 5 years ago

b167809a

feat(meta/expr): add parser for generated binder names (#4540)

JLimperg committed 5 years ago

fcaf6e91

chore(algebra/big_operators/basic): add lemma prod_multiset_count' that generalize prod_multiset_count to consider a function to a monoid (#4534)

riccardobrasca committed 5 years ago

306dc8a0

chore(topology/instances/nnreal): use notation (#4548)

urkud committed 5 years ago

656ef0a5

lint(various): nolint has_inhabited_instance for injective functions (#4541)

hrmacbeth committed 5 years ago

d0f45f52

chore(data/nat/cast): a few `simp`/`norm_cast` lemmas (#4549)

urkud committed 5 years ago

cc75e4ef

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

leanprover-community-bot committed 5 years ago

f6836c16

chore(topology/algebra/group): move a lemma to `group_theory/coset` (#4522)

urkud committed 5 years ago

8004fb68

feat(topology/basic): add `is_open_iff_ultrafilter` (#4529)

urkud committed 5 years ago

ce999a89

fix(bors.toml, build.yml): check for new linter, rename linter to "Lint style" (#4539)

gebner committed 5 years ago

a9124551

refactor(category_theory/pairwise): change direction of morphisms in the category of pairwise intersections (#4537)

kim-em committed 5 years ago

73f119e0

fix(update-copy-mod-doc-exceptions.sh): cleanup, sort properly (#4533)

bryangingechen committed 5 years ago

0ae4a3d5

chore(algebra/monoid_algebra): Fix TODO about unwanted unfolding (#4532)

eric-wieser committed 5 years ago

427564e0

chore(data/padics/*): linting + squeeze_simp speedup (#4531)

jcommelin committed 5 years ago

0c18d968

feat(data/equiv/*): to_monoid_hom_injective and to_ring_hom_injective (#4525)

ChrisHughes24 committed 5 years ago

60be8ed5

lint(computability/halting): docstrings (#4524)

awainverse committed 5 years ago

253f2252

chore(*): add a few more `unique` instances (#4511)

urkud committed 5 years ago

e74bd261

feat(archive/imo): revive @kbuzzard's imo2019_q1 (#4377)

dselsam committed 5 years ago

7b42c714

feat(number_theory/arithmetic_function): define `is_multiplicative` on `arithmetic_function`s, provides examples (#4312)

awainverse committed 5 years ago

9b0d30c0

lint(multiset/pi): remove unused instance (#4526)

awainverse committed 5 years ago

5a01549f

feat(logic/nontrivial): a tactic to summon nontrivial instances (#4374)

kim-em committed 5 years ago

48a36046

chore(algebra/char_zero): rename vars, add `with_top` instance (#4523)

urkud committed 5 years ago

43f52dd7

chore(data/quot): `quot.mk` etc are surjective (#4517)

urkud committed 5 years ago

34a44717

chore(*/hom,equiv): Split `monoid_hom` into more fundamental structures, and reuse them elsewhere (#4423)

eric-wieser committed 5 years ago

4f757600

ci(*): run style lint in parallel job, fix update-copy-mod-doc-exceptions.sh (#4513)

bryangingechen committed 5 years ago

b4dc9128

feat(data/polynomial/degree/trailing_degree): fixed formatting and streamlined a couple of proofs (#4509)

adomani committed 5 years ago

3d1d4fbe

doc(tactic/slim_check): improve advice in error message (#4520)

cipher1024 committed 5 years ago

7a715545

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

leanprover-community-bot committed 5 years ago

e9d1dc47

chore(topology/algebra/monoid,group): rename variables (#4516)

urkud committed 5 years ago

a5b0376c

Newer Older