leanprover-community/mathlib3

Pull Requests Commits

feat(data/polynomial/degree/trailing_degree): basic definitions and properties (#4113)

adomani committed 5 years ago

caffd024

feat(topology/sheaves): alternate formulation of the sheaf condition (#4190)

kim-em committed 5 years ago

58d0bfcc

feat(l1_space): add measurability to integrable (#4170)

fpvandoorn committed 5 years ago

b4641efe

refactor(ring_theory/unique_factorization_domain): completes the refactor of `unique_factorization_domain` (#4156)

awainverse committed 5 years ago

2ae199f1

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

leanprover-community-bot committed 5 years ago

480c92cd

chore(topology/algebra/module): make `topological_module` an abbreviation (#4200)

urkud committed 5 years ago

b91df551

chore(data/nat/digits): use nat namespace (#4201)

ChrisHughes24 committed 5 years ago

92c01257

chore(category_theory/limits/lattice): cleanup (#4191)

kim-em committed 5 years ago

4a8c38e4

fix(scripts/mk_all): macOS compatibility fix (#4148)

alexpeattie committed 5 years ago

cd4a91f7

feat(ring_theory/unique_factorization_domain): API for coprime, coprime factor of a power is a power (#4049)

paulvanwamelen committed 5 years ago

e483298a

feat(data/*/nat_antidiagonal): induction lemmas about antidiagonals (#4193)

awainverse committed 5 years ago

40f582b9

feat(tactic/tauto): optional closer tactic for `tauto` (#4189)

Jesse Michael Han committed 5 years ago

d8e7bb56

feat(data/finset): add lemma for empty filter (#4188)

b-mehta committed 5 years ago

f77d5d6f

feat(analysis/calculus/times_cont_diff): inversion of continuous linear maps is smooth (#4185)

hrmacbeth committed 5 years ago

db9842c8

feat(topology/path_connected): add lemmas about paths and continuous families of paths (#4063)

PatrickMassot committed 5 years ago

d774ef68

feat(measure_theory): Borel-Cantelli (#4166)

TwoFX committed 5 years ago

884e90be

feat(algebra/big_operators): add prod boole lemma (#4192)

b-mehta committed 5 years ago

2c9b0634

feat(ring_theory/power_series): power series lemmas (#4171)

b-mehta committed 5 years ago

44667ba6

refactor(linear_algebra/tensor_algebra): build as a quotient of a free algebra (#4079)

kim-em committed 5 years ago

9232032b

feat(category_theory/internal): commutative monoid objects (#4186)

kim-em committed 5 years ago

7013e5b7

feat(data/set/basic): a few lemmas (#4184)

mzinkevi committed 5 years ago

5b143ff1

feat(geometry/euclidean): cospherical points (#4178)

jsm28 committed 5 years ago

640ba6c8

feat(category_theory/Mon): Mon_ C has limits when C does (#4133)

kim-em committed 5 years ago

02b492ab

feat(category_theory): `lim : (J ⥤ C) ⥤ C` is lax monoidal when `C` is monoidal (#4132)

kim-em committed 5 years ago

567954fa

feat(algebra/ring_quot): quotients of noncommutative rings (#4078)

kim-em committed 5 years ago

04fe4b6d

fix(conditionally_complete_lattice): add instance (#4183)

fpvandoorn committed 5 years ago

bf7a2ed3

doc(simps): explain short_name (#4182)

fpvandoorn committed 5 years ago

c2ae6c0e

feat(integration): integral commutes with continuous linear maps (#4167)

PatrickMassot committed 5 years ago

0269a76e

feat(geometry/euclidean/basic): intersections of circles (#4088)

jsm28 committed 5 years ago

4e3729b8

feat(polynomial): prepare for transcendence of e by adding small lemmas (#4175)

jjaassoonn committed 5 years ago

9051aa73

Newer Older