leanprover-community/mathlib

Pull Requests Commits

feat(category_theory): quotient categories (#2310)

dwarn committed 5 years ago

Verified 906874e2

feat(group_theory/monoid_localization): some homs induced on localizations: lift, map (#2118)

101damnations committed 5 years ago

Verified a590d4b5

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

6af5901b

refactor(tactic/lint): split into multiple files (#2299)

gebner committed 5 years ago

Verified 8af4bb8d

feat(order/filter): add lemmas about `∀ᶠ`, `∃ᶠ` and logic operations (#2314)

urkud committed 5 years ago

Verified cb0a1b50

chore(test/*): move tests into individual files (#2317)

kim-em committed 5 years ago

Verified 1b24e0a0

fix(tactic/lint): simp_nf: do not ignore errors (#2266)

gebner committed 5 years ago

Verified d3b8622b

feat(logic/basic): a few lemmas about `exists_unique` (#2283)

urkud committed 5 years ago

Verified 654533ff

chore(topology/metric_space): use dot notation (#2313)

urkud committed 5 years ago

Verified a88356ff

feat(algebra/pi_instances): bundled homs for apply and single (#2186)

kim-em committed 5 years ago

Verified 3c27d284

chore(category_theory/concrete_category): take an instance, rather than extending, category (#2195)

kim-em committed 5 years ago

Verified 313cc2fe

refactor(*): move `algebra` below `polynomial` in the `import` chain (#2294)

urkud committed 5 years ago

Verified f55e3ce4

chore(data/set/lattice): add `set_of_exists` and `set_of_forall` (#2312)

urkud committed 5 years ago

Verified 652fc17a

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

5b972be7

chore(tactic/transport): rename to transform_decl (#2308)

kim-em committed 5 years ago

Verified 33764abc

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

badc615e

refactor(data/real/irrational): review (#2304)

urkud committed 5 years ago

Verified a8076b2c

feat(tactic/simp_rw): support `<-` in `simp_rw` (#2309)

Vierkantor committed 5 years ago

Verified 203ebb20

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

fb658acd

chore(algebra/module): cleanup `is_linear_map` (#2296)

urkud committed 5 years ago

Verified 003141c8

refactor(group_theory/submonoid): review API (#2173)

urkud committed 5 years ago

Verified c7fb84ba

fix(algebra/category): make has_coe_to_sort instances for bundled categories reducible (#2290)

kim-em committed 5 years ago

Verified 67e7f90d

feat(data/nat/basic): `simp` lemmas about inequalities with `bit*` (#2207)

urkud committed 5 years ago

Verified cc20a865

feat(data/fintype/card): prod_univ_sum (#2284)

ChrisHughes24 committed 5 years ago

Verified 7d89f2ea

feat(data/finset): card_image_le (#2295)

digama0 committed 5 years ago

Verified 224ba7e0

feat(tactic/equiv_rw): incorporating equiv_functor (#2301)

kim-em committed 5 years ago

Verified 72d3b6e3

feat(tactic/equiv_rw): rewriting along equivalences (#2246)

kim-em committed 5 years ago

Verified b508d0e0

feat(data/monoid_algebra): some lemmas about group rings (#2239)

kim-em committed 5 years ago

Verified 26690624

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

17632202

refactor(*): migrate more files to bundled `ring_hom`s (#2286)

urkud committed 5 years ago

Verified 85affa45

Newer Older