leanprover-community/mathlib

Pull Requests Commits

kim-em committed 5 years ago

4df952d1

feat(data/set/basic): +2 lemmas, +2 `simp` attrs (#3182)

urkud committed 5 years ago

2d270ff1

chore(*): last preparations for Heine (#3179)

PatrickMassot committed 5 years ago

ef62d1c0

feat(algebra/big_operators): telescoping sums (#3184)

jalex-stark committed 5 years ago

6624509e

almost there, but need more from noncommutative polynomials

kim-em committed 5 years ago

b8b69276

Merge remote-tracking branch 'origin/master' into polynomial_tensor2

kim-em committed 5 years ago

231b6c19

key lemma about evaluation of noncommutative polynomials

kim-em committed 5 years ago

eaec54db

feat(ring_theory/matrix_equiv_tensor): matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R) (#3177)

kim-em committed 5 years ago

5b97da63

kim-em committed 5 years ago

01799187

chore(category/*): linting (#3178)

kim-em committed 5 years ago

3cfc0e73

feat(data/fintype): trunc_sigma_of_exists (#3166)

kim-em committed 5 years ago

c3923e39

chore(category_theory/equivalence) explicit transitivity transformation (#3176)

b-mehta committed 5 years ago

616cb5e6

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

leanprover-community-bot committed 5 years ago

abae5a3c

feat(tactic/abel) teach abel to gsmul_zero (#3173)

alexjbest committed 5 years ago

43a2b24d

refactor(ring_theory/ideals): make local_ring a prop class (#3171)

kbuzzard committed 5 years ago

db7a53af

feat(category/default): comp_dite (#3163)

kim-em committed 5 years ago

afc1c24e

feat(category_theory/limits): isos from reindexing limits (#3100)

kim-em committed 5 years ago

c6f629bc

feat(*): bump to Lean 3.16.5 (#3170)

kim-em committed 5 years ago

158e84ae

chore(*): assorted lemmas about `set` and `finset` (#3158)

urkud committed 5 years ago

7d331eb9

feat(category_theory): show a pullback of a regular mono is regular (#2780)

b-mehta committed 5 years ago

80a08778

feat(filter, topology): cluster_pt and principal notation, redefine compactness (#3160)

PatrickMassot committed 5 years ago

3f868fab

feat(category/adjunction): missing simp lemmas (#3168)

kim-em committed 5 years ago

e7db701e

chore(category/discrete): missing simp lemmas (#3165)

kim-em committed 5 years ago

d86f1c83

chore(category/equivalence): cleanup (#3164)

kim-em committed 5 years ago

266d3163

feat(category/preadditive): comp_sum (#3162)

kim-em committed 5 years ago

e8187ac1

feat(data/quot): add `map'`, `hrec_on'`, and `hrec_on₂'` (#3148)

urkud committed 5 years ago

3875012a

feat(algebra/big_operators): prod_dite_eq (#3167)

kim-em committed 5 years ago

553e4534

refactor(algebra/*): small API fixes (#3157)

urkud committed 5 years ago

8f04a92a

feat(archive/100-theorems-list/73_ascending_descending_sequences): Erdős–Szekeres (#3074)

b-mehta committed 5 years ago

e1a72b50

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

leanprover-community-bot committed 5 years ago

5c7e1a22

Newer Older