leanprover-community/mathlib3

Pull Requests Commits

full and faithful;

b-mehta committed 5 years ago

Verified 18fc3b56

b-mehta committed 5 years ago

Verified 3f91353e

chore(logic/basic): add a few `simp` lemmas (#5278)

urkud committed 5 years ago

3996bd42

chore(combinatorics/composition): use `order_embedding` (#5276)

urkud committed 5 years ago

d3bbaeb9

chore(group_theory/perm): Add alternate formulation of (sum|sigma)_congr lemmas (#5260)

eric-wieser committed 5 years ago

51f5ca3e

chore(*): move/add lemmas about `disjoint` (#5277)

urkud committed 5 years ago

ac6fc38e

chore(data/list/sort): docs, add a few lemmas (#5274)

urkud committed 5 years ago

ef377a92

feat(category_theory/monad): generalise algebra colimits (#5234)

b-mehta committed 5 years ago

aec64b17

feat(category_theory/closed/types): presheaf category is cartesian closed (#4897)

b-mehta committed 5 years ago

73601789

chore(data/list/pairwise): add `list.pairwise_pmap` and `list.pairwise.pmap` (#5273)

urkud committed 5 years ago

8f42d73d

chore(data/support): zero function has empty support (#5275)

urkud committed 5 years ago

3f4829cd

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

leanprover-community-bot committed 5 years ago

35f08626

refactor(data/fin): use `order_embedding` for many maps (#5251)

urkud committed 5 years ago

b173925a

feat(topology/algebra/infinite_sum): add lemmas about continuous linear maps (#5243)

dupuisf committed 5 years ago

b9689bdc

chore(logic/basic): add `and.congr_left_iff` and `@[simp]` attrs (#5268)

urkud committed 5 years ago

f7301374

feat(dynamics/circle/rotation_number): translation numbers define a group action up to a semiconjugacy (#5138)

urkud committed 5 years ago

44400c99

feat(analysis/mean_inequalities): add young_inequality for nnreal and ennreal with real exponents (#5242)

RemyDegenne committed 5 years ago

f0ceb6bb

chore(topology/category/Profinite): Fix docstring (#5265)

adamtopaz committed 5 years ago

914d2b13

feat(order/filter/ultrafilter): Restriction of ultrafilters along large embeddings (#5195)

adamtopaz committed 5 years ago

b2427d53

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

leanprover-community-bot committed 5 years ago

67eb675c

chore(topology/algebra/ordered): generalize `intermediate_value_Icc` etc (#5235)

urkud committed 5 years ago

8d54d527

chore(ring_theory/algebra_tower): generalize `is_scalar_tower.right` (#5224)

urkud committed 5 years ago

9cb27c94

feat(number_theory/primes_congruent_one): infinitely many primes congruent to 1 (#5217)

riccardobrasca committed 5 years ago

128b316c

feat(combinatorics/simple_graph/basic): introduce incidence sets, graph construction from relation (#5191)

agusakov committed 5 years ago

b3aa0524

refactor(*): drop `topology/instances/complex` (#5208)

urkud committed 5 years ago

c88e8f35

feat(ring_theory/witt_vector): common identities between operators on Witt vectors (#5161)

jcommelin committed 5 years ago

29a1731a

chore(*): clean up several unnecessary let statements (#5257)

alexjbest committed 5 years ago

339bd9a9

feat(data/polynomial): simp lemmas about polynomial derivatives (#5256)

alexjbest committed 5 years ago

12a8361f

chore(algebra/group_power): mark `map_pow` etc as `@[simp]` (#5253)

urkud committed 5 years ago

c6de6e4f

doc(data/list): fix `erasep` doc string (#5254)

robertylewis committed 5 years ago

85380712

Older