leanprover-community/mathlib

Pull Requests Commits

feat(data/nat/basic): inequalities (#2801)

kim-em committed 5 years ago

9bb99568

feat(category_theory/limits): transport lemmas for kernels (#2779)

TwoFX committed 5 years ago

4b616e6d

fix(group_with_zero): fix definition of comm_monoid_with_zero (#2818)

fpvandoorn committed 5 years ago

aad2dfc4

feat(algebra/ring): ring_hom.map_dvd (#2813)

ChrisHughes24 committed 5 years ago

ae5b55bd

feat(data/polynomial): is_unit_C (#2812)

ChrisHughes24 committed 5 years ago

52b839f3

feat(linear_algebra/projection): add `equiv_prod_of_surjective_of_is_compl` (#2787)

urkud committed 5 years ago

3e0668e0

feat(logic/function): define `semiconj` and `commute` (#2788)

urkud committed 5 years ago

60f0b012

feat(algebra/group_power): int.nat_abs_pow_two (#2811)

ChrisHughes24 committed 5 years ago

96f318c5

feat(data/zmod): lemmas about coercions to zmod (#2802)

kim-em committed 5 years ago

9da47ada

feat(data/nat/prime): pow_not_prime (#2810)

ChrisHughes24 committed 5 years ago

dd062f02

chore(topology/algebra/module): prove `fst.prod snd = id` (#2806)

urkud committed 5 years ago

a2d50075

chore(set_theory/ordinal): use a `protected lemma` to drop a `nolint` (#2805)

urkud committed 5 years ago

ccf646d3

fix(tactic/norm_num): workaround int.sub unfolding bug (#2804)

digama0 committed 5 years ago

a3b3aa62

feat(algebra/add_torsor): torsors of additive group actions (#2720)

jsm28 committed 5 years ago

6552f21e

feat(data/int/basic): eq_zero_of_dvd_of_nonneg_of_lt (#2803)

kim-em committed 5 years ago

518d0fd9

feat(char_p): generalize zmod.neg_one_ne_one (#2796)

kim-em committed 5 years ago

8d352b20

chore(scripts): update nolints.txt (#2799)

leanprover-community-bot committed 5 years ago

61b57cd7

chore(scripts): update nolints.txt (#2798)

leanprover-community-bot committed 5 years ago

1445e088

feat(category_theory): Product comparison (#2753)

b-mehta committed 5 years ago

8590081f

feat(category_theory): adjunction convenience defs (#2754)

b-mehta committed 5 years ago

292fc042

feat(linear_algebra/basic): range of `linear_map.prod` (#2785)

urkud committed 5 years ago

2ef444af

chore(order/basic): change "minimum" in descriptions to "minimal" (#2789)

kckennylau committed 5 years ago

5449203f

doc(archive/100-theorems-list): Update README.md (#2750)

jalex-stark committed 5 years ago

79e296bd

chore(scripts): update nolints.txt (#2782)

leanprover-community-bot committed 5 years ago

2a3f59a1

feat(ring_theory/ideal_operations): lemmas about ideals and galois connections (#2767)

ChrisHughes24 committed 5 years ago

2b79f1da

chore(order/basic): add `monotone.order_dual`, `strict_mono.order_dual` (#2778)

urkud committed 5 years ago

ceb13bad

feat(data/fintype): finset.univ_map_embedding (#2765)

kim-em committed 5 years ago

90abd3bb

feat(data/polynomial): prime_of_degree_eq_one_of_monic (#2745)

ChrisHughes24 committed 5 years ago

69485051

chore(data/equiv): make `equiv.ext` args use { } (#2776)

urkud committed 5 years ago

8c1793fe

chore(scripts): update nolints.txt (#2777)

leanprover-community-bot committed 5 years ago

f66caaad

Newer Older