leanprover-community/mathlib3

Pull Requests Commits

chore(topology/list): one import per line (#4479)

jcommelin committed 5 years ago

ac058890

chore(*): add copyright headers (#4477)

jcommelin committed 5 years ago

e559ca98

feat(data/polynomial/ring_division): add multiplicity of sum of polynomials is at least minimum of multiplicities (#4442)

riccardobrasca committed 5 years ago

74161277

feat(*): make `int.le` irreducible (#4474)

robertylewis committed 5 years ago

8d199395

chore(parity): even and odd in semiring (#4473)

PatrickMassot committed 5 years ago

99e308d3

chore(data/mv_polynomial/basic): coeff_mul, more golfing and speedup (#4472)

jcommelin committed 5 years ago

1d1a0415

chore(algebra/algebra): Split subalgebras into their own file (#4471)

eric-wieser committed 5 years ago

8cebd2b1

lint(logic/unique): module doc, docstring (#4461)

jcommelin committed 5 years ago

94bc31d3

lint(group_theory/eckmann_hilton): docs, module docs, unused argument (#4459)

jcommelin committed 5 years ago

2fc65980

feat(data/*): lemmas about lists and finsets (#4457)

urkud committed 5 years ago

f4207aa2

chore(category_theory/monoidal): add module docs (#4454)

kim-em committed 5 years ago

1fa07c2c

feat(geometry/euclidean/monge_point): orthocentric systems (#4448)

jsm28 committed 5 years ago

4d9406e2

lint(data/equiv/ring): docstrings, inhabited (#4460)

jcommelin committed 5 years ago

e9b43b6a

chore(category_theory/*): doc-strings (#4453)

kim-em committed 5 years ago

58a54d34

chore(control/traversable/{basic,equiv,instances,lemmas}): linting (#4444)

kmill committed 5 years ago

6b59725c

feat(data/finsupp): lift a collection of `add_monoid_hom`s to an `add_monoid_hom` on `α →₀ β` (#4395)

urkud committed 5 years ago

372d2949

chore(data/mv_polynomial/basic): speedup coeff_mul (#4469)

jcommelin committed 5 years ago

b1d3ef9a

feat(trailing_degree): added two lemmas support_X, support_X_empty computing the support of X, simplified a couple of lemmas (#4294)

adomani committed 5 years ago

c08a8686

feat(normed_space/basic): remove localized notation (#4246)

fpvandoorn committed 5 years ago

fc7e943e

chore(topology/compacts): inhabit instances (#4462)

hrmacbeth committed 5 years ago

32b5b68d

lint(measure_theory): docstrings and style (#4455)

fpvandoorn committed 5 years ago

d3b1d65d

doc(data/nat/prime, data/int/basic, data/int/modeq): docstrings (#4445)

awainverse committed 5 years ago

523bddb4

lint(category_theory/monad): doc-strings (#4428)

kim-em committed 5 years ago

cd785998

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

leanprover-community-bot committed 5 years ago

a228af6a

lint(category_theory/limits): docstrings and inhabited instances (#4435)

TwoFX committed 5 years ago

27b6c239

feat(undergrad): minimal polynomial (#4308)

PatrickMassot committed 5 years ago

37879aa6

feat(measure_theory/integration): add lintegral_with_density_eq_lintegral_mul (#4350)

mzinkevi committed 5 years ago

432da5f8

lint(topology/algebra): docstrings (#4446)

PatrickMassot committed 5 years ago

97c444e0

lint(data/pnat): Docstrings and an unused argument in `pnat.basic`, `pnat.factors` (#4443)

awainverse committed 5 years ago

21158c43

lint(src/order/rel_iso): docstrings and inhabited (#4441)

b-mehta committed 5 years ago

45347f93

Newer Older