leanprover-community/mathlib

Pull Requests Commits

alreadydone committed 4 years ago

e7c3f69c

Merge branch 'adjunction_mates' into Gillam

alreadydone committed 4 years ago

19df6688

adjunction/mates: new lemmas/easy defs

alreadydone committed 4 years ago

d2bac998

Presheaf: ongoing work

alreadydone committed 4 years ago

109a8952

PresheafedSpace: functors and adjunction

alreadydone committed 4 years ago

7e058b1d

define PrimedPreringedSpace and functor from LRS

alreadydone committed 4 years ago

8c9dcad2

Merge branch 'misc_1113' into Gillam

alreadydone committed 4 years ago

2d16da63

forgot to add an important part with another def

alreadydone committed 4 years ago

af8e3ce7

Merge branch 'misc_1113' into Gillam

alreadydone committed 4 years ago

6d788c99

alreadydone committed 4 years ago

9167c12b

Merge branch 'misc_1113' into Gillam

alreadydone committed 4 years ago

7cb903c6

address comments

alreadydone committed 4 years ago

5b5e1220

Merge branch 'misc_1113' into PRS_loc

alreadydone committed 4 years ago

15f57489

alreadydone committed 4 years ago

16eddd54

Merge branch 'misc_1113' into PRS_loc

alreadydone committed 4 years ago

731ef7ab

Miscellaneous defs/lemmas

alreadydone committed 4 years ago

3c8b55b7

define category PrimedPreringedSpace

alreadydone committed 4 years ago

ab6225d8

feat(category_theory/sites/plus): If P is a sheaf, then the map from P to P^+ is an isomorphism. (#10297)

adamtopaz committed 4 years ago

8bb0b6f7

feat(data/nat/basic): recursion for set nat (#10273)

stuart-presnell committed 4 years ago

55534c4f

feat(analysis/inner_product_space/spectrum): diagonalization of self-adjoint endomorphisms (finite dimension) (#9995)

hrmacbeth committed 4 years ago

6afda884

feat(category_theory/sites/sheaf): Add sheaf conditions in terms of multiforks/multiequalizers. (#10294)

adamtopaz committed 4 years ago

f0a98494

chore(analysis/special_functions/trigonometric/complex): put results about derivatives into a new file (#10156)

RemyDegenne committed 4 years ago

adb5c2d6

feat(analysis/normed_space/continuous_affine_map): isometry from space of continuous affine maps to product of codomain with space of continuous linear maps (#10201)

ocfnash committed 4 years ago

62621659

fix(algebra/graded_monoid): correct nonexistent names in tactic defaults (#10293)

eric-wieser committed 4 years ago

b9f7b4db

chore(linear_algebra/multilinear): add const_of_is_empty (#10291)

eric-wieser committed 4 years ago

d7b5ffa0

doc(field_theory/separable): typo (#10290)

ericrbg committed 4 years ago

c5027c91

feat(group_theory/complement): `is_complement'.sup_eq_top` (#10230)

tb65536 committed 4 years ago

6cd63207

doc(README): add list of emeritus maintainers (#10288)

jcommelin committed 4 years ago

07be9042

feat(category_theory/sites/plus): `P⁺` for a presheaf `P`. (#10284)

adamtopaz committed 4 years ago

b51335c4

feat(measure_theory): define `measurable_space` instance on a quotient (#10275)

urkud committed 4 years ago

e6790930

Older