leanprover-community/mathlib3

Pull Requests Commits

chore(ci): teach bors and GitHub about new labels (#4146)

robertylewis committed 5 years ago

8877606b

feat(measure_theory): assorted integration lemmas (#4145)

PatrickMassot committed 5 years ago

49fc7edd

feat(linear_algebra/finite_dimensional): finite-dimensional submodule lemmas / instances (#4128)

jsm28 committed 5 years ago

5f45c0c6

chore(category_theory/*): make all forgetful functors use explicit arguments (#4139)

kim-em committed 5 years ago

d5c58eb8

feat(algebra/category/Module): the monoidal category of R-modules is symmetric (#4140)

kim-em committed 5 years ago

a998fd10

refactor(data/nat/*): cleanup data.nat.basic, split data.nat.choose (#4135)

bryangingechen committed 5 years ago

e35e287b

chore(data/polynomial/derivative): golf proof of mem_support_derivative (#4134)

shingtaklam1324 committed 5 years ago

39962b7c

feat(category_theory): Mon_.forget reflects isos (#4131)

kim-em committed 5 years ago

6756d47c

feat(data/mv_polynomial/monad): mv_polynomial is a monad in two different ways (#4080)

jcommelin committed 5 years ago

bbfeff38

feat(computability/tm_computable): define computable (in polytime) for TMs, prove id is computable in constant time (#4048)

MadPidgeon committed 5 years ago

ed71b2df

chore(algebra/homology): cleanup instances post #3995 (#4137)

kim-em committed 5 years ago

dce6b373

feat(field_theory/fixed): dimension over fixed field is order of group (#4125)

kckennylau committed 5 years ago

1c2ddbcf

doc(measure_theory): docstrings for continuity from above and below (#4122)

TwoFX committed 5 years ago

b1e5a6b6

doc(category_theory/natural_isomorphism): documentation and cleanup (#4120)

kim-em committed 5 years ago

5a478f0d

feat(linear_algebra/affine_space,geometry/euclidean): simplex centers and order of points (#4116)

jsm28 committed 5 years ago

51608f4a

feat(ring_theory/algebra_tower): coefficients for a basis in an algebra tower (#4114)

Vierkantor committed 5 years ago

b19fbd79

chore(category_theory/limits): remove unnecessary typeclass arguments (#4141)

kim-em committed 5 years ago

e3559335

chore(category_theory/limits/functor_category): shuffle limits in functor cats (#4124)

b-mehta committed 5 years ago

bd385fbf

feat(algebraic_geometry/*): Gamma the global sections functor (#4126)

kckennylau committed 5 years ago

5d35e626

feat(category_theory/limits/types): is_limit versions of limits in type (#4130)

b-mehta committed 5 years ago

f403a8be

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

leanprover-community-bot committed 5 years ago

dd43823c

feat(normed_space): second countability for linear maps (#4099)

PatrickMassot committed 5 years ago

f3326db1

fix(algebra/ring/basic): delete mul_self_sub_mul_self_eq (#4119)

bryangingechen committed 5 years ago

c8771b6b

feat(slim_check): add test cases (#4100)

cipher1024 committed 5 years ago

169384a7

doc(group_theory/subgroup): fix links in module doc (#4115)

bryangingechen committed 5 years ago

c3a6a699

chore(category_theory): minor cleanups (#4110)

kim-em committed 5 years ago

88dd01b7

feat(logic/basic): Add more simp lemmas for forall (#4117)

eric-wieser committed 5 years ago

b1a210ec

feat(category_theory/limits): make has_limit a Prop (#3995)

kim-em committed 5 years ago

34199869

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

leanprover-community-bot committed 5 years ago

f6a65cff

feat(logic/basic): Add forall_apply_eq_imp_iff (#4109)

eric-wieser committed 5 years ago

7bade58b

Newer Older