leanprover-community/mathlib

Pull Requests Commits
feat(list/basic): list.subset_singleton_iff (#16183)
ericrbg committed 3 years ago
4970a17c
chore(algebra/order/monoid): move lemmas (#16176)
urkud committed 3 years ago
cf7b16a6
feat(data/rat/cast): drop an unneeded typeclass assumption (#15972)
urkud committed 3 years ago
6a5a2b13
feat(data/sym/basic): add nil coe lemma (#16181)
pimotte committed 3 years ago
07052296
feat(algebra/order/ring): generalize some `mono` lemmas, use them (#14691)
urkud committed 3 years ago
bfd28571
feat(*): rsuffices golfs (#16159)
ericrbg committed 3 years ago
6155d435
refactor(analysis/convex/basic): Redefine convexity in terms of star-convexity (#16173)
YaelDillies committed 3 years ago
0da54467
chore(analysis/inner_product_space): move `is_symmetric` to a new file lower in the import tree (#16106)
ADedecker committed 3 years ago
90bc9579
feat(data/set/prod): decidable mem instance on set prod (#16107)
dtumad committed 3 years ago
175a0959
Add `prime.eq_of_factorization_pos`
stuart-presnell committed 3 years ago
5a92929e
Fill in docstrings
stuart-presnell committed 3 years ago
8bfdc877
Move lemmas
stuart-presnell committed 3 years ago
bfc3a341
Rename lemma
stuart-presnell committed 3 years ago
39b9d0b6
Golf proofs
stuart-presnell committed 3 years ago
6f1afde7
Move and golf lemmas
stuart-presnell committed 3 years ago
8e65dbc9
Move lemma; add docstrings
stuart-presnell committed 3 years ago
09a8957b
Rename lemmas
stuart-presnell committed 3 years ago
5e11750c
Add drafts of three new lemmas
stuart-presnell committed 3 years ago
c79e32c3
feat(algebra/*): Algebraic instances on `lex`/`order_dual` (#16122)
YaelDillies committed 3 years ago
e0b2fa6d
refactor(data/int/cast): Use hom classes (#16024)
YaelDillies committed 3 years ago
972aa423
chore(scripts): update nolints.txt (#16179)
leanprover-community-bot committed 3 years ago
b46c8953
chore(algebra/big_operators/pi): rename `w` to `H` in assumptions (#16166)
urkud committed 3 years ago
ec73f6e3
feat(group_theory/coset): Right cosets are orbits (#16119)
tb65536 committed 3 years ago
aac3141e
feat(set_theory/cardinal/finite): `nat.card (zmod n) = n` (#16118)
tb65536 committed 3 years ago
eaeb4583
feat(algebraic_topology): split simplicial objects (#16072)
joelriou committed 3 years ago
df967907
feat(algebra/order/complete_field): generalize ring_hom_monotone (#16147)
alreadydone committed 3 years ago
ee261437
refactor(order/minimals): Change definition to `a ≤ b → b ≤ a` (#16103)
YaelDillies committed 3 years ago
67488dff
chore(field_theory/*): Fix lint (#16149)
YaelDillies committed 3 years ago
c2c31b52
feat(data/finset/pointwise): `-s • t = -(s • t)` (#16138)
YaelDillies committed 3 years ago
4a0f332e
split(analysis/convex/segment): Split off `analysis/convex.basic` (#16112)
YaelDillies committed 3 years ago
4705dd0d
Terms Of Use Privacy Policy Refund Policy Impressum