leanprover-community/mathlib

Pull Requests Commits
feat(order/filter): add lemmas about `∀ᶠ`, `∃ᶠ` and logic operations (#2314)
urkud committed 6 years ago
Verified cb0a1b50
chore(test/*): move tests into individual files (#2317)
kim-em committed 6 years ago
Verified 1b24e0a0
fix(tactic/lint): simp_nf: do not ignore errors (#2266)
gebner committed 6 years ago
Verified d3b8622b
feat(logic/basic): a few lemmas about `exists_unique` (#2283)
urkud committed 6 years ago
Verified 654533ff
chore(topology/metric_space): use dot notation (#2313)
urkud committed 6 years ago
Verified a88356ff
feat(algebra/pi_instances): bundled homs for apply and single (#2186)
kim-em committed 6 years ago
Verified 3c27d284
chore(category_theory/concrete_category): take an instance, rather than extending, category (#2195)
kim-em committed 6 years ago
Verified 313cc2fe
refactor(*): move `algebra` below `polynomial` in the `import` chain (#2294)
urkud committed 6 years ago
Verified f55e3ce4
chore(data/set/lattice): add `set_of_exists` and `set_of_forall` (#2312)
urkud committed 6 years ago
Verified 652fc17a
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
5b972be7
chore(tactic/transport): rename to transform_decl (#2308)
kim-em committed 6 years ago
Verified 33764abc
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
badc615e
refactor(data/real/irrational): review (#2304)
urkud committed 6 years ago
Verified a8076b2c
feat(tactic/simp_rw): support `<-` in `simp_rw` (#2309)
Vierkantor committed 6 years ago
Verified 203ebb20
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
fb658acd
chore(algebra/module): cleanup `is_linear_map` (#2296)
urkud committed 6 years ago
Verified 003141c8
refactor(group_theory/submonoid): review API (#2173)
urkud committed 6 years ago
Verified c7fb84ba
fix(algebra/category): make has_coe_to_sort instances for bundled categories reducible (#2290)
kim-em committed 6 years ago
Verified 67e7f90d
feat(data/nat/basic): `simp` lemmas about inequalities with `bit*` (#2207)
urkud committed 6 years ago
Verified cc20a865
feat(data/fintype/card): prod_univ_sum (#2284)
ChrisHughes24 committed 6 years ago
Verified 7d89f2ea
feat(data/finset): card_image_le (#2295)
digama0 committed 6 years ago
Verified 224ba7e0
feat(tactic/equiv_rw): incorporating equiv_functor (#2301)
kim-em committed 6 years ago
Verified 72d3b6e3
feat(tactic/equiv_rw): rewriting along equivalences (#2246)
kim-em committed 6 years ago
Verified b508d0e0
feat(data/monoid_algebra): some lemmas about group rings (#2239)
kim-em committed 6 years ago
Verified 26690624
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
17632202
refactor(*): migrate more files to bundled `ring_hom`s (#2286)
urkud committed 6 years ago
Verified 85affa45
feat(analysis/analytic): first take on analytic functions (#2199)
sgouezel committed 6 years ago
Verified 66f30901
chore(scripts): update nolints.txt
leanprover-community-bot committed 6 years ago
20bff2c7
refactor(data/fintype): move data/fintype to data/fintype/basic (#2285)
ChrisHughes24 committed 6 years ago
Verified 4168aba3
feat(*): more `prod`-related (continuous) linear maps and their derivatives (#2277)
urkud committed 6 years ago
Verified c5181d11
Terms Of Use Privacy Policy Refund Policy Impressum