leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' into eric-wieser/perm-move

eric-wieser committed 5 years ago

Verified d0d1433a

chore(data/quot): Add missing simp lemmas (#5372)

eric-wieser committed 5 years ago

6548be43

chore(*): use notation `ℝ≥0` (#5391)

urkud committed 5 years ago

78940f46

feat(algebra/lie/basic): nilpotent and solvable Lie algebras (#5382)

Oliver Nash committed 5 years ago

47b3c4b4

feat(equiv/basic): add true_arrow_equiv (#5388)

fpvandoorn committed 5 years ago

79e9aeed

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

leanprover-community-bot committed 5 years ago

26f8b288

feat(tactic/ext): `ext?` displays applied lemmas (#5375)

Jesse Michael Han committed 5 years ago

e264e5f4

feat(category_theory/isomorphism): is_iso versions (#5355)

b-mehta committed 5 years ago

2ee0f1ef

feat(topology/separation): add lemma connected_component_eq_clopen_Inter (#5335)

callesonne committed 5 years ago

dbb6b043

chore(algebra/category/Module/monoidal): Speed up the elaboration (#5383)

eric-wieser committed 5 years ago

66eddd8b

feat(ring_theory/roots_of_unity): add squarefreeness mod p of minimal polynomial (#5381)

riccardobrasca committed 5 years ago

b7024088

ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter (#5330)

bryangingechen committed 5 years ago

78e48c02

feat(analysis/mean_inequalities): add Minkowski's inequality for the Lebesgue integral of ennreal functions (#5379)

RemyDegenne committed 5 years ago

c208a651

fix(group_theory/subgroup): Fix doubly-namespaced instance (#5378)

eric-wieser committed 5 years ago

3a997b1d

feat(data/set/basic): nonempty set of nonempty subtype (#5373)

pechersky committed 5 years ago

75130b39

feat(ring_theory/roots_of_unity): minimal polynomial of primitive roots (#5322)

riccardobrasca committed 5 years ago

d21d17b1

feat(category_theory/limits): product comparison simp lemmas (#5351)

b-mehta committed 5 years ago

0f4ac1bf

chore(category_theory/sites): improve naming (#5350)

b-mehta committed 5 years ago

9ba9a983

feat(group_theory/perm/basic): Bundle sigma_congr_right and sum_congr into monoid_homs (#5301)

eric-wieser committed 5 years ago

dd72a981

feat(category_theory/monad): monadicity theorems (#5137)

b-mehta committed 5 years ago

8041945f

chore(category_theory/equivalence): weaken essential surjectivity (#3821)

b-mehta committed 5 years ago

407d1386

feat(simps): interaction between simps and to_additive (#5331)

fpvandoorn committed 5 years ago

a1aa5110

chore(algebra/quadratic_discriminant): golf proofs using limits (#5339)

urkud committed 5 years ago

a959718e

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

leanprover-community-bot committed 5 years ago

ff13cdeb

feat(group_theory/subgroup): Add decidable_mem_range (#5371)

eric-wieser committed 5 years ago

cadaa44a

fix(group_theory): Remove a duplicate fintype instance on quotient_group.quotient (#5368)

eric-wieser committed 5 years ago

b2ab94f8

chore(topology/instances/ennreal): remove summability assumption in tendsto_sum_nat_add (#5366)

sgouezel committed 5 years ago

b364d337

chore(data/finsupp/basic): more lemmas about `α →₀ ℕ` (#5362)

urkud committed 5 years ago

4dbb3e23

chore(order/iterate): generalize lemmas about inequalities and iterations (#5357)

urkud committed 5 years ago

8de08f72

refactor(measure_theory/lp_space): move most of the proof of mem_Lp.add to a new lemma in analysis/mean_inequalities (#5370)

RemyDegenne committed 5 years ago

d1904fce

Older