leanprover-community/mathlib

Pull Requests Commits

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

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

leanprover-community-bot committed 5 years ago

065bd5fc

style(combinatorics/simple_graph/basic): edit proof of lemma to match style guidelines (#5245)

agusakov committed 5 years ago

7e8e174b

feat(field_theory/galois): Is_galois iff is_galois bot (#5231)

tb65536 committed 5 years ago

ae99c76d

chore(data/multiset/basic): make `card` a bundled `add_monoid_hom` (#5228)

urkud committed 5 years ago

ddfba423

chore(data/equiv/ring): add `symm_symm` and `coe_symm_mk` (#5227)

urkud committed 5 years ago

1f648141

fix(topology/algebra/infinite_sum): fix docstring typos and add example (#5159)

kbuzzard committed 5 years ago

d4bd4cda

feat(category_theory/limits): morphisms to equalizer (#5233)

b-mehta committed 5 years ago

83b13d1c

chore(linear_algebra/basic): redefine `restrict` (#5229)

urkud committed 5 years ago

dd114987

chore(data/prod): `prod.swap` is `bijective` (#5226)

urkud committed 5 years ago

481f5e09

chore(data/equiv/basic): Add missing refl/trans/symm simp lemmas (#5223)

eric-wieser committed 5 years ago

c5009dd7

chore(category_theory/limits/preserves): make names consistent (#5240)

b-mehta committed 5 years ago

3972da8a

feat(order/filter/at_top_bot): `order_iso` maps `at_top` to `at_top` (#5236)

urkud committed 5 years ago

39a3b58b

chore(category_theory/limits): preserving coequalizers (#5212)

b-mehta committed 5 years ago

147a81a2

Newer Older