leanprover-community/mathlib3

Pull Requests Commits
fix
yuma-mizuno committed 3 years ago
630246c6
wip
yuma-mizuno committed 3 years ago
4bf1b464
adjointiry
yuma-mizuno committed 3 years ago
5edb998a
revert the last commit
yuma-mizuno committed 3 years ago
d36fc588
Revert "Prop valued `bicategorical_coherence`"
yuma-mizuno committed 3 years ago
b69e8568
Prop valued `bicategorical_coherence`
yuma-mizuno committed 3 years ago
33dfcb16
wip
yuma-mizuno committed 3 years ago
12749085
wip
yuma-mizuno committed 3 years ago
40e3fec9
wip
yuma-mizuno committed 3 years ago
b3ff7e93
wip
yuma-mizuno committed 3 years ago
411f4a04
fix
yuma-mizuno committed 3 years ago
f61b8838
add coherence tactic
yuma-mizuno committed 3 years ago
3329b48a
canonical 2-morphism
yuma-mizuno committed 3 years ago
a4c95f2c
golf
yuma-mizuno committed 3 years ago
40c0fb8e
new proof of `oplax_nat_trans.vcomp`
yuma-mizuno committed 3 years ago
6de3506c
rearrange lemmas
yuma-mizuno committed 3 years ago
668a857a
golf
yuma-mizuno committed 3 years ago
aac1f066
golf
yuma-mizuno committed 3 years ago
ffb2694f
associator free proof in stric bicategory
yuma-mizuno committed 3 years ago
61d52491
remove unused files
yuma-mizuno committed 3 years ago
1f1ff836
modify import
yuma-mizuno committed 3 years ago
265b11dd
golf
yuma-mizuno committed 3 years ago
9f70cdd9
change simp direction for `left_unitor_comp`
yuma-mizuno committed 3 years ago
89062aed
golf
yuma-mizuno committed 3 years ago
fb0a2a71
wip
yuma-mizuno committed 3 years ago
456a7897
tidy up
yuma-mizuno committed 3 years ago
a8b6ff41
reduce parentheses
yuma-mizuno committed 3 years ago
8ebd8dfc
increase precedence of whisker
yuma-mizuno committed 3 years ago
324ce93c
tidy up
yuma-mizuno committed 3 years ago
17854ed5
minor rearrange
yuma-mizuno committed 3 years ago
169f5dbc
Terms Of Use Privacy Policy Refund Policy Impressum