leanprover-community/mathlib3

Pull Requests Commits

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

feat(control/traversable/basic): composition of applicative transformations (#4487)

kmill committed 5 years ago

93cdc3a5

lint(ring_theory/*): docstrings (#4485)

awainverse committed 5 years ago

fe8b6315

lint(order/bounded_lattice): docstring (#4484)

hrmacbeth committed 5 years ago

7488f8ef

feat(data/nat/basic): add_succ_lt_add (#4483)

jsm28 committed 5 years ago

f4ccbdf5

feat(measure_theory): integral of a non-negative function is >0 iff μ(support f) > 0 (#4410)

urkud committed 5 years ago

f88234d1

feat(data/polynomial/degree/basic): add lemmas dealing with monomials, their support and their nat_degrees (#4475)

adomani committed 5 years ago

5192fd94

feat(ring_theory/witt_vector/structure_polynomial): witt_structure_rat{_prop} (#4464)

jcommelin committed 5 years ago

d768e46f

Newer Older