leanprover-community/mathlib

Pull Requests Commits

alexjbest committed 4 years ago

aadc3aea

alexjbest committed 4 years ago

546a7f09

alexjbest committed 4 years ago

c74d64c2

alexjbest committed 4 years ago

93d99e81

alexjbest committed 4 years ago

a6a6a1ad

alexjbest committed 4 years ago

4e0e31e7

alexjbest committed 4 years ago

48974001

alexjbest committed 4 years ago

5dbf1739

alexjbest committed 4 years ago

3025851d

alexjbest committed 4 years ago

c0e1851d

alexjbest committed 4 years ago

3599eead

vasconcelos was PRed

alexjbest committed 4 years ago

5acfc9b2

alexjbest committed 4 years ago

1ff8414c

alexjbest committed 4 years ago

ac637f9b

alexjbest committed 4 years ago

43a318f4

try to refresh last part seeing as one result is already in mathlib

alexjbest committed 4 years ago

03fa6187

Merge branch 'master' of github.com:leanprover-community/mathlib into alexjbest/dedekind-finite

alexjbest committed 4 years ago

3feb4743

alexjbest committed 4 years ago

e3ddaa40

alexjbest committed 4 years ago

4e761dff

feat(docs/references) : Added reference for #10791 (#10915)

erdOne committed 4 years ago

c40c7013

feat(data/finset/basic): add image_congr (#10911)

AntoineChambert-Loir committed 4 years ago

9cbd828a

refactor(ring_theory/tensor_product): Speed up slow proofs (#10883)

tb65536 committed 4 years ago

f7b24fa7

chore(category_theory/filtered): avoid `finish` (#10918)

Ruben-VandeVelde committed 4 years ago

6ab0f909

feat(algebra/algebra/subalgebra): `subalgebra.map` commutes with supremum (#10899)

tb65536 committed 4 years ago

5dd35377

Merge branch 'master' of github.com:leanprover-community/mathlib into alexjbest/dedekind-finite

alexjbest committed 4 years ago

278eca1c

feat(ring_theory/tensor_product): The tensor product `A ⊗ B` is generated by tensors `a ⊗ₜ b` (#10900)

tb65536 committed 4 years ago

41ced1ca

feat(order/monotone): add `monotone_int_of_le_succ` etc (#10895)

urkud committed 4 years ago

194bde8f

feat(data/list/sort): subperm sorted implies sublist (#10892)

b-mehta committed 4 years ago

a60ef7c9

feat (order/lexicographic): add API lemmas (#10887)

MantasBaksys committed 4 years ago

faee3582

chore(order/complete_lattice): eliminate `finish` (#10876)

stuart-presnell committed 4 years ago

45ed9ded

Older