leanprover-community/mathlib

Pull Requests Commits

adamtopaz committed 4 years ago

6b69979c

Add initial/terminal defs

adamtopaz committed 4 years ago

b13f2ddf

adamtopaz committed 4 years ago

2aff975e

Add comments + linting

adamtopaz committed 4 years ago

13c12662

Some cleanup + add adjunction

adamtopaz committed 4 years ago

a38bd849

Lan equiv finished

adamtopaz committed 4 years ago

1fcd1e1e

adamtopaz committed 4 years ago

c27dd3ac

A bit of cleanup

adamtopaz committed 4 years ago

56f6d186

adamtopaz committed 4 years ago

0e6ec6dd

Start on cleanup

adamtopaz committed 4 years ago

c48fc557

Add adjunction.

adamtopaz committed 4 years ago

671815f2

This is getting a bit messy...

adamtopaz committed 4 years ago

b1c517cb

Start on right Kan

adamtopaz committed 4 years ago

e0e40115

b-mehta committed 4 years ago

Verified d6456c0d

Merge branch 'master' into right-kan

b-mehta committed 4 years ago

Verified fde353b5

refactor(algebraic_topology/simplex_category): Make simplex_category universe polymorphic. (#6761)

adamtopaz committed 4 years ago

695d7f4f

refactor(category_theory/cones): golf and cleanup cones (#6756)

b-mehta committed 4 years ago

4db82a40

feat(category_theory/closed): currying rfl lemmas (#6754)

b-mehta committed 4 years ago

56e5aa74

fix(analysis/special_functions/integrals): move lemmas out of namespace (#6778)

benjamindavidson committed 4 years ago

b0150a5d

feat(topology): continuous_pi_iff pi.has_continuous_mul pi.topological_group (#6689)

agjftucker committed 4 years ago

26fcfbc9

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

leanprover-community-bot committed 4 years ago

07282da6

feat(dynamics/ergodic): define measure preserving maps (#6764)

urkud committed 4 years ago

b4a2991c

feat(data/real/pi): Wallis product for pi (#6568)

winston-h-zhang committed 4 years ago

eba4829b

chore(data/finset/basic): erase_inj_on (#6769)

pechersky committed 4 years ago

c65146d6

feat(measure_theory): define Hausdorff measure and Hausdorff dimension (#6710)

urkud committed 4 years ago

2d2929f8

feat(analysis/special_functions/exp_log): log_nonzero_of_ne_one and log_inj_pos (#6734)

thejohncrafter committed 4 years ago

152412ff

feat(ring_theory/multiplicity): Multiplicity with units (#6729)

thejohncrafter committed 4 years ago

6f3e0ad1

refactor(linear_algebra/basic): move the lattice structure to its own file (#6767)

eric-wieser committed 4 years ago

591c34b6

feat(analysis/special_functions/integrals): integrating linear combinations of functions (#6597)

benjamindavidson committed 4 years ago

ce107da5

docs(category_theory): missing module docs (#6752)

kim-em committed 4 years ago

590f43db

Older