leanprover-community/mathlib3

Pull Requests Commits
refactor(measure_theory): add typeclasses for measurability of operations (#6832)
urkud committed 4 years ago
0e4760b3
functoriality
kim-em committed 4 years ago
44bdfd18
functoriality of boundaries
kim-em committed 4 years ago
57b4563c
minor
kim-em committed 4 years ago
bfa86569
lint(*): split long lines (#6918)
urkud committed 4 years ago
dc34b216
functoriality for cycles
kim-em committed 4 years ago
9f4d030f
change to design
kim-em committed 4 years ago
f3694a07
cleanup
kim-em committed 4 years ago
073393a9
better
kim-em committed 4 years ago
dc35b015
chore(scripts): update nolints.txt (#6917)
leanprover-community-bot committed 4 years ago
e129117c
minor
kim-em committed 4 years ago
a9e3e0d1
Merge branch 'homology2' of github.com:leanprover-community/mathlib into homology2
kim-em committed 4 years ago
6f40d7a5
minor
kim-em committed 4 years ago
7517a924
bit more progress
kbuzzard committed 4 years ago
0e7e034d
Merge branch 'homology2' into complex_ses
kbuzzard committed 4 years ago
4dcc2711
tidy up (thanks Bhavik)
kbuzzard committed 4 years ago
e99e1db2
epsilon more
kbuzzard committed 4 years ago
45c1ae52
feat(test/integration): add examples of computing integrals by simp (#6859)
benjamindavidson committed 4 years ago
879cb474
a bit more (thanks Kenny)
kbuzzard committed 4 years ago
c8728f6d
chore(category_theory/monads): remove empty file (#6915)
b-mehta committed 4 years ago
06b21d0f
refactor(geometry/manifold/algebra/smooth_functions): make `smooth_map_group` division defeq to `pi.has_div` (#6912)
ocfnash committed 4 years ago
27c86764
homology of a complex of modules
kbuzzard committed 4 years ago
1494d6a9
category structure
kbuzzard committed 4 years ago
0ade1f88
add hom structure
kbuzzard committed 4 years ago
e15c7573
chore(topology/metric_space): golf, generalize, rename (#6849)
urkud committed 4 years ago
d1044139
fix import
kbuzzard committed 4 years ago
a9c9e65f
rearrange
kim-em committed 4 years ago
eda922d6
trying again
kim-em committed 4 years ago
690ebc20
refactor(representation_theory/maschke): replaces `¬(ring_char k ∣ fintype.card G)` with `invertible (fintype.card G : k)` instance (#6901)
awainverse committed 4 years ago
cc7e722a
feat(data/nat/log): add some lemmas and monotonicity (#6899)
hallow-world committed 4 years ago
d32f9c72
Terms Of Use Privacy Policy Refund Policy Impressum