leanprover-community/mathlib3

Pull Requests Commits

Add file free.lean

adamtopaz committed 5 years ago

fbe49ec9

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

feat(category_theory/limits/fubini): another formulation for limits commuting (#4034)

kim-em committed 5 years ago

17a58072

feat(topology/sheaves): sheafification (#3937)

kim-em committed 5 years ago

045619ea

feat(category_theory/skeleton): add skeletal categories and construct a special case (#3929)

b-mehta committed 5 years ago

5509a30a

feat(geometry/euclidean/circumcenter): lemmas on orthogonal projection and reflection (#4087)

jsm28 committed 5 years ago

847f87ee

cleanup(group_theory/presented_group): () -> [], and remove some FIXMEs (#4076)

kim-em committed 5 years ago

872a37e4

feat(category_theory/braided): braiding and unitors (#4075)

kim-em committed 5 years ago

377c7c91

feat(logic/basic, logic/function/basic): involute ite (#4074)

pechersky committed 5 years ago

a1cbe88a

feat(data/{sym2,sym}) decidable version of sym2.mem.other, filling out some of sym API (#4008)

kmill committed 5 years ago

832acd63

feat(category_theory/monoidal): lax monoidal functors take monoids to monoids (#4108)

kim-em committed 5 years ago

7886c27b

feat(algebra/homology/exact): lemmas about exactness (#4106)

kim-em committed 5 years ago

bd74baa1

feat(algebraic_geometry/Scheme): Spec as Scheme (#4104)

kckennylau committed 5 years ago

233a802c

feat(nnreal): absolute value (#4098)

PatrickMassot committed 5 years ago

34e0f313

feat(category_theory): the Grothendieck construction (#3896)

kim-em committed 5 years ago

842a3246

doc(category_theory): add doc-strings and links to the stacks project (#4107)

kim-em committed 5 years ago

0c57b2da

chore(*): use new `extends_priority` default of 100, part 2 (#4101)

rwbarton committed 5 years ago

3965e063

feat(geometry/euclidean/monge_point): reflection of circumcenter (#4062)

jsm28 committed 5 years ago

bc78621a

feat(category_theory/limits): filtered colimits commute with finite limits (in Type) (#4046)

kim-em committed 5 years ago

4ce27a5d

refactor(data/mv_polynomial/pderivative): make pderivative a linear map (#4095)

shingtaklam1324 committed 5 years ago

80a9e4f4

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

leanprover-community-bot committed 5 years ago

9a24f689

feat(ring_theory/algebra_operations): add le_div_iff_mul_le (#4102)

kbuzzard committed 5 years ago

7d88b314

feat(data/fin): iffs about succ_above ordering (#4092)

pechersky committed 5 years ago

e33a777d

chore(*): update to Lean 3.20.0c, account for nat.pow removal from core (#3985)

rwbarton committed 5 years ago

38d1715b

refactor(data/mv_polynomial): move `smul` lemmas into basic.lean (#4097)

shingtaklam1324 committed 5 years ago

d5be9f38

feat(data/mv_polynomial): a few facts about `constant_coeff` and `aeval` (#4085)

robertylewis committed 5 years ago

19b9ae6e

feat(slim_check): make `shrink` recursive (#4038)

cipher1024 committed 5 years ago

d857def3

feat(data/{int,nat}/cast): dvd cast lemmas (#4086)

robertylewis committed 5 years ago

55cab6c0

feat(ring_theory/dedekind_domain): definitions (#4000)

knaka3435 committed 5 years ago

49bb92dc

Older