leanprover-community/mathlib

Pull Requests Commits

First version of the tactic

TwoFX committed 4 years ago

4a11b647

Fix the remaining things and restore Bhavik's proof

TwoFX committed 4 years ago

10c57eb0

Break everything

TwoFX committed 4 years ago

84ed63f6

attempt to use the embedding into endofunctors to prove coherence

kim-em committed 4 years ago

5530b8bd

all homs are iso

b-mehta committed 4 years ago

Verified 2888455e

add a couple of lemmas and finish proof

b-mehta committed 4 years ago

Verified 9a02fc55

An attempt at coherence

TwoFX committed 4 years ago

6b70e30f

Merge remote-tracking branch 'origin/master' into drinfeld_2

kim-em committed 4 years ago

64d7daed

kim-em committed 4 years ago

d9eeda8c

chore(category_theory/subobject): different proof of le_of_comm (#7229)

TwoFX committed 4 years ago

206ecce7

feat(order/conditionally_complete_lattice): conditional Inf of intervals (#7226)

b-mehta committed 4 years ago

0f6c1f19

feat(category_theory): formally adjoined initial objects are strict (#7222)

TwoFX committed 4 years ago

560a0092

complete construction of braided monoidal structure

kim-em committed 4 years ago

c82f23ff

chore(ring_theory/adjoin.basic): use submodule.closure in algebra.adjoin_eq_span (#7194)

riccardobrasca committed 4 years ago

89c16a79

feat(test/integration): improve an example (#7169)

benjamindavidson committed 4 years ago

b7a3d4e1

kim-em committed 4 years ago

5f81eeb6

Merge branch 'drinfeld_1' into drinfeld_2

kim-em committed 4 years ago

d8fff95d

Merge remote-tracking branch 'origin/master' into drinfeld_1

kim-em committed 4 years ago

355d9e47

add missing axiom, oops

kim-em committed 4 years ago

82dff4a1

feat(category_theory/triangulated/pretriangulated): add definition of pretriangulated categories and triangulated functors between them (#7153)

l-kershaw committed 4 years ago

6b182fcd

feat(data/list/basic): fold[rl] recursion principles (#7079)

pechersky committed 4 years ago

110541dd

feat(data/set): sep true/false simp lemmas (#7215)

b-mehta committed 4 years ago

49040e50

feat(data/finsupp/basic): add finsupp.single_left_injective and docstrings (#7207)

eric-wieser committed 4 years ago

24013e2b

feat(order/rel_iso): constructors for rel embeddings (#7046)

b-mehta committed 4 years ago

06886125

feat(category_theory): the additive envelope, Mat_ C (#6845)

kim-em committed 4 years ago

ea4dce03

that was probably the worst on the way to monoidal

kim-em committed 4 years ago

a3933c6c

chore(algebra): add `sub{_mul_action,module,semiring,ring,field,algebra}.copy` (#7220)

eric-wieser committed 4 years ago

108b9235

chore(group_theory/subgroup): rename `monoid_hom.to_range` to `monoid_hom.range_restrict` (#7218)

eric-wieser committed 4 years ago

e00d688f

kim-em committed 4 years ago

db8cb56f

kim-em committed 4 years ago

211457ea

Older