leanprover-community/mathlib

Pull Requests Commits

an attempt at building canonical isomorphisms between different parenthesisations

kim-em committed 6 years ago

939662ad

Merge branch 'master' into monoidal-categories

kim-em committed 6 years ago

Verified 83090976

Scott Morrison committed 6 years ago

d2d198a2

chore(CommRing/adjunctions): refactor proofs (#1049)

kim-em committed 6 years ago

62acd6b8

doc(finsupp,category_theory): fixes (#1075)

fpvandoorn committed 6 years ago

15fecbdd

feat(linear_algebra/basic): general_linear_group basics (#1064)

jcommelin committed 6 years ago

d07e3b3e

feat(data/nat): various lemmas (#1017)

kim-em committed 6 years ago

f004d327

Scott Morrison committed 6 years ago

f40de11d

Merge branch 'master' into monoidal-categories

kim-em committed 6 years ago

Verified 7aa02c81

renaming, and namespaces

Scott Morrison committed 6 years ago

722ebdcf

Scott Morrison committed 6 years ago

b5ff7514

Scott Morrison committed 6 years ago

e3a47d58

feat(*): image_closure (#1069)

jcommelin committed 6 years ago

971ddcc2

refactor(integration.lean): changing `measure_space` to `measurable_space` (#1072)

kodyvajjha committed 6 years ago

34613996

feat(algebra/pi_instances): product of submonoids/groups/rings (#1066)

jcommelin committed 6 years ago

cb30c97e

feat(category_theory): limits in CommRing (#1006)

kim-em committed 6 years ago

0ab8a89d

chore(topology/algebra/monoid): continuous_mul_left/right (#1065)

jcommelin committed 6 years ago

8cf7c4c8

chore(ring_theory/algebra): simp-lemmas for alg_hom.to_linear_map (#1062)

jcommelin committed 6 years ago

593938cd

feat(tactic/basic): adds `contrapose` tactic (#1015)

PatrickMassot committed 6 years ago

d001abfd

feat(topology/opens): continuous.comap : opens Y → opens X (#1061)

jcommelin committed 6 years ago

15a6af22

feat(tactic/linarith): better input syntax linarith only [...] (#1056)

robertylewis committed 6 years ago

d4c7b7a6

refactor: coherent composition order (#1055)

sgouezel committed 6 years ago

f2534017

refactor(topology/metric/gromov_hausdorff): make Hausdorff_edist irreducible (#1052)

sgouezel committed 6 years ago

cb4c9ee7

feat(topology/order): make nhds irreducible (#1043)

robertylewis committed 6 years ago

b9cb69c3

kim-em committed 6 years ago

a23ce189

kim-em committed 6 years ago

8f4ad436

kim-em committed 6 years ago

d1db8d70

notations for associator, unitors?

kim-em committed 6 years ago

59eb2358

temporary notations

kim-em committed 6 years ago

d221522b

Merge commit '73c3f71741552159a36388a1ab5cc2bcfd64459a' into monoidal-categories

kim-em committed 6 years ago

f0e05a2b

Older