leanprover-community/mathlib

Pull Requests Commits

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

Merge branch 'ordered_semiring_zero_le_one' into bell

kim-em committed 5 years ago

739fea99

Apply suggestions from code review

kim-em committed 5 years ago

Verified adef1076

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

kim-em committed 5 years ago

5de128bc

kim-em committed 5 years ago

245e0e98

kim-em committed 5 years ago

39848f05

Merge branch 'nontriviality' into ordered_semiring_zero_le_one

kim-em committed 5 years ago

39e1ad2d

Merge remote-tracking branch 'origin/master' into nontriviality

kim-em committed 5 years ago

454e2400

take optional type argument

kim-em committed 5 years ago

d27dfd02

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

leanprover-community-bot committed 5 years ago

e9d1dc47

kim-em committed 5 years ago

bd287bf2

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

urkud committed 5 years ago

a5b0376c

Newer Older