leanprover-community/mathlib3

Pull Requests Commits

A take on submodule_functor by jmc

jcommelin committed 6 years ago

ddbec3aa

Scott Morrison committed 6 years ago

a3d685fd

Scott Morrison committed 6 years ago

51519765

Scott Morrison committed 6 years ago

337f5126

building functors

Scott Morrison committed 6 years ago

2940db79

trying to write a functorial is_local

Scott Morrison committed 6 years ago

43bb700c

kim-em committed 6 years ago

e4d4a0ab

experiments with core

kim-em committed 6 years ago

fd8ac614

just use large_category, to escape universe hell??

Scott Morrison committed 6 years ago

940eb868

making a horrible mess...

Scott Morrison committed 6 years ago

8f5ff153

test cases for iso_induction

kim-em committed 6 years ago

211771de

removing [irreducible] on core

Scott Morrison committed 6 years ago

60e51250

defining the core of a category

kim-em committed 6 years ago

a57206a8

about to define the core of a category

kim-em committed 6 years ago

86df6603

kim-em committed 6 years ago

a7cc1118

feat(category_theory): working in Sort rather than Type, as far as possible

kim-em committed 6 years ago

efa2e000

refactor(*): rename metric_space_subtype to subtype.metric_space (#817)

jcommelin committed 6 years ago

2bf44d31

feat(topology/metric_space/baire): Baire theorem (#816)

sgouezel committed 6 years ago

c5afc52a

feat(tactic/squeeze,hole): remove needless qualifications in names

cipher1024 committed 6 years ago

72100bd5

feat(data/list|multiset|finset): lemmas about intervals in nat (#795)

kim-em committed 6 years ago

82f79a58

chore(topology/*): @uniformity α _ becomes 𝓤 α (#814)

PatrickMassot committed 6 years ago

2738f9b4

feat(tactic/basic): folding over the environment, to get all declarations (#798)

kim-em committed 6 years ago

33602670

feat(data/alist,data/finmap): union (#750)

spl committed 6 years ago

bde8690e

feat(topology/algebra/group): extensionality for top group structure

Patrick Massot committed 6 years ago

eb96a25d

feat(topology/algebra/monoid): add is_submonoid.mem_nhds_one (#809)

kbuzzard committed 6 years ago

69249d8b

refactor(data/list): rm redundant eq_nil_of_forall_not_mem (#804)

spl committed 6 years ago

51c31cea

feat(data/set/finite): add finite_lt_nat (#807)

kbuzzard committed 6 years ago

e8818faf

feat(ring_theory/noetherian): Nakayama's Lemma (#778)

kckennylau committed 6 years ago

7de57e84

refactot(data/equiv/basic): rename apply_inverse_apply to apply_symm_apply (#800)

ChrisHughes24 committed 6 years ago

1159fa95

style(data/list/basic): clean up count_bag_inter

robertylewis committed 6 years ago

b1af1402

Older