leanprover-community/mathlib

Pull Requests Commits
merge
kim-em committed 3 years ago
488f2dfb
Merge remote-tracking branch 'origin/master' into pnat
kim-em committed 3 years ago
0f8aa6a5
fix downstream imports
kim-em committed 3 years ago
55f89285
fix downstream imports
kim-em committed 3 years ago
6ae95dd5
chore(scripts): update nolints.txt (#17363)
leanprover-community-bot committed 3 years ago
22fe10de
chore(analysis/*): remove some non-terminal simps (#17346)
mcdoll committed 3 years ago
97265543
chore(linear_algebra/finsupp): golf `finsupp.lcongr_symm` (#17341)
eric-wieser committed 3 years ago
83f7236b
merge
kim-em committed 3 years ago
425fb24f
merge
kim-em committed 3 years ago
f93ff044
chore(algebra/order/field): don't import finiteness hierarchy (#17350)
kim-em committed 3 years ago
ef0ef216
fixes
kim-em committed 3 years ago
63ed1dbb
getting there
kim-em committed 3 years ago
391bcfcc
Merge branch 'split_order_group' into split_order_ring
kim-em committed 3 years ago
c566284e
Merge remote-tracking branch 'origin/master' into split_order_group
kim-em committed 3 years ago
69d99a55
merge
kim-em committed 3 years ago
507e1652
fix
kim-em committed 3 years ago
f275d41f
feat(data/(d)finsupp): well-foundedness of lexicographic and product orders (#16772)
alreadydone committed 3 years ago
e9b8651e
initial split
kim-em committed 3 years ago
7533e6fe
add downstream imports
kim-em committed 3 years ago
a5c37779
Merge remote-tracking branch 'origin/field_fintype' into order_field_power
kim-em committed 3 years ago
ef72d2cc
fix topology.algebra.order.basic
YaelDillies committed 3 years ago
75ccc563
Update src/algebra/order/field/pi.lean
kim-em committed 3 years ago
Verified a1b1c992
Merge remote-tracking branch 'origin/master' into pnat
kim-em committed 3 years ago
e4de83c2
simp linter
kim-em committed 3 years ago
66941a06
module-doc
kim-em committed 3 years ago
91e87b63
oops
kim-em committed 3 years ago
ddeec9d8
fix linear_algebra.affine_space.affine_map
YaelDillies committed 3 years ago
8f852862
chore(data/polynomial/degree): golf a proof (#17322)
urkud committed 3 years ago
59386b20
feat(combinatorics/simple_graph/connectivity): `is_bridge` and cycle characterization (#17306)
kmill committed 3 years ago
d3abacf0
chore(algebra/ne_zero): move the dependencies out (#17177)
digama0 committed 3 years ago
9f78ea86
Terms Of Use Privacy Policy Refund Policy Impressum