leanprover-community/mathlib

Pull Requests Commits

feat(tactic/converter): Add an exact tactic, to allow dropping back into tactic mode

eric-wieser committed 5 years ago

ec4cb37d

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

chore(algebra/pointwise): add `###` here and there (#4514)

urkud committed 5 years ago

d67062f4

chore(topology/*): use dot notation for `is_open.prod` and `is_closed.prod` (#4510)

urkud committed 5 years ago

fa8b7ba2

chore(ring_theory/coprime): weaken assumptions of finset.prod_dvd_of_coprime (#4506)

jcommelin committed 5 years ago

2b89d59b

chore(algebra/continuous_functions): `coninuous` -> `continuous` (#4508)

Jesse Michael Han committed 5 years ago

4635aee7

fix(data/list/defs): remove map_head; rename map_last to modify_last (#4507)

JLimperg committed 5 years ago

4e8427ec

doc(data/num/basic): added doc-strings to most defs (#4439)

shingtaklam1324 committed 5 years ago

a4a20ac3

feat(data/matrix): add `matrix.mul_sub` and `matrix.sub_mul` (#4505)

Vierkantor committed 5 years ago

8f9c10fc

chore(*big_operators*): line length (#4504)

gebner committed 5 years ago

2d34e94a

fix(tactic/ring): use int_sub_hack to avoid defeq blowup (#4503)

digama0 committed 5 years ago

6b50fb99

ci(scripts/*): linting for copyright, imports, module docstrings, line length (#4486)

jcommelin committed 5 years ago

4db1c72f

lint(data/matrix/basic): add definition docstrings (#4478)

ADedecker committed 5 years ago

c9d4567e

fix(tactic/doc_commands): do not construct json by hand (#4501)

gebner committed 5 years ago

6a852793

chore(data/tree): linting (#4499)

kmill committed 5 years ago

0386adaf

lint(category_theory/equivalence): docstring and a module doc (#4495)

TwoFX committed 5 years ago

cbbc123e

feat(ring_theory/witt_vector/structure_polynomial): {map_}witt_structure_int (#4465)

jcommelin committed 5 years ago

8a4b491c

chore(data/quot): linting (#4500)

kmill committed 5 years ago

e5ce9d3d

chore(*): normalise copyright headers (#4497)

jcommelin committed 5 years ago

ed9ef1b4

lint(group_theory/*): docstrings and an inhabited instance (#4493)

awainverse committed 5 years ago

3c755273

lint(group_theory/perm/*): docstrings (#4492)

awainverse committed 5 years ago

8c528b9a

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

leanprover-community-bot committed 5 years ago

cb3118d5

lint(order/lexographic, pilex): docstrings (#4489)

awainverse committed 5 years ago

2e77ef6a

lint(order/order_iso_nat): docstrings (#4488)

awainverse committed 5 years ago

afffab1d

Older